MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvrn0 Structured version   Unicode version

Theorem fvrn0 5870
Description: A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011.) (Revised by Stefan O'Rear, 3-Jan-2015.)
Assertion
Ref Expression
fvrn0  |-  ( F `
 X )  e.  ( ran  F  u.  {
(/) } )

Proof of Theorem fvrn0
StepHypRef Expression
1 id 22 . . 3  |-  ( ( F `  X )  =  (/)  ->  ( F `
 X )  =  (/) )
2 ssun2 3654 . . . 4  |-  { (/) } 
C_  ( ran  F  u.  { (/) } )
3 0ex 4569 . . . . 5  |-  (/)  e.  _V
43snid 4044 . . . 4  |-  (/)  e.  { (/)
}
52, 4sselii 3486 . . 3  |-  (/)  e.  ( ran  F  u.  { (/)
} )
61, 5syl6eqel 2550 . 2  |-  ( ( F `  X )  =  (/)  ->  ( F `
 X )  e.  ( ran  F  u.  {
(/) } ) )
7 ssun1 3653 . . 3  |-  ran  F  C_  ( ran  F  u.  {
(/) } )
8 fvprc 5842 . . . . 5  |-  ( -.  X  e.  _V  ->  ( F `  X )  =  (/) )
98con1i 129 . . . 4  |-  ( -.  ( F `  X
)  =  (/)  ->  X  e.  _V )
10 fvex 5858 . . . . 5  |-  ( F `
 X )  e. 
_V
1110a1i 11 . . . 4  |-  ( -.  ( F `  X
)  =  (/)  ->  ( F `  X )  e.  _V )
12 fvbr0 5869 . . . . . 6  |-  ( X F ( F `  X )  \/  ( F `  X )  =  (/) )
1312ori 373 . . . . 5  |-  ( -.  X F ( F `
 X )  -> 
( F `  X
)  =  (/) )
1413con1i 129 . . . 4  |-  ( -.  ( F `  X
)  =  (/)  ->  X F ( F `  X ) )
15 brelrng 5221 . . . 4  |-  ( ( X  e.  _V  /\  ( F `  X )  e.  _V  /\  X F ( F `  X ) )  -> 
( F `  X
)  e.  ran  F
)
169, 11, 14, 15syl3anc 1226 . . 3  |-  ( -.  ( F `  X
)  =  (/)  ->  ( F `  X )  e.  ran  F )
177, 16sseldi 3487 . 2  |-  ( -.  ( F `  X
)  =  (/)  ->  ( F `  X )  e.  ( ran  F  u.  {
(/) } ) )
186, 17pm2.61i 164 1  |-  ( F `
 X )  e.  ( ran  F  u.  {
(/) } )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1398    e. wcel 1823   _Vcvv 3106    u. cun 3459   (/)c0 3783   {csn 4016   class class class wbr 4439   ran crn 4989   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-cnv 4996  df-dm 4998  df-rn 4999  df-iota 5534  df-fv 5578
This theorem is referenced by:  fvssunirn  5871  dfac4  8494  dfac2  8502  dfacacn  8512  axdc2lem  8819  axcclem  8828  ccatfnOLD  12583  plusffval  16079  staffval  17694  scaffval  17728  lpival  18091  ipffval  18859  nmfval  21278  tchex  21829  tchnmfval  21840  orderseqlem  29575  rrnval  30566  lsatset  35131
  Copyright terms: Public domain W3C validator