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

Theorem fvrn0 6677
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 (𝐹𝑋) ∈ (ran 𝐹 ∪ {∅})

Proof of Theorem fvrn0
StepHypRef Expression
1 id 22 . . 3 ((𝐹𝑋) = ∅ → (𝐹𝑋) = ∅)
2 ssun2 4103 . . . 4 {∅} ⊆ (ran 𝐹 ∪ {∅})
3 0ex 5178 . . . . 5 ∅ ∈ V
43snid 4564 . . . 4 ∅ ∈ {∅}
52, 4sselii 3915 . . 3 ∅ ∈ (ran 𝐹 ∪ {∅})
61, 5eqeltrdi 2901 . 2 ((𝐹𝑋) = ∅ → (𝐹𝑋) ∈ (ran 𝐹 ∪ {∅}))
7 ssun1 4102 . . 3 ran 𝐹 ⊆ (ran 𝐹 ∪ {∅})
8 fvprc 6642 . . . . 5 𝑋 ∈ V → (𝐹𝑋) = ∅)
98con1i 149 . . . 4 (¬ (𝐹𝑋) = ∅ → 𝑋 ∈ V)
10 fvexd 6664 . . . 4 (¬ (𝐹𝑋) = ∅ → (𝐹𝑋) ∈ V)
11 fvbr0 6676 . . . . . 6 (𝑋𝐹(𝐹𝑋) ∨ (𝐹𝑋) = ∅)
1211ori 858 . . . . 5 𝑋𝐹(𝐹𝑋) → (𝐹𝑋) = ∅)
1312con1i 149 . . . 4 (¬ (𝐹𝑋) = ∅ → 𝑋𝐹(𝐹𝑋))
14 brelrng 5779 . . . 4 ((𝑋 ∈ V ∧ (𝐹𝑋) ∈ V ∧ 𝑋𝐹(𝐹𝑋)) → (𝐹𝑋) ∈ ran 𝐹)
159, 10, 13, 14syl3anc 1368 . . 3 (¬ (𝐹𝑋) = ∅ → (𝐹𝑋) ∈ ran 𝐹)
167, 15sseldi 3916 . 2 (¬ (𝐹𝑋) = ∅ → (𝐹𝑋) ∈ (ran 𝐹 ∪ {∅}))
176, 16pm2.61i 185 1 (𝐹𝑋) ∈ (ran 𝐹 ∪ {∅})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1538  wcel 2112  Vcvv 3444  cun 3882  c0 4246  {csn 4528   class class class wbr 5033  ran crn 5524  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-cnv 5531  df-dm 5533  df-rn 5534  df-iota 6287  df-fv 6336
This theorem is referenced by:  fvssunirn  6678  dfac4  9537  dfac2b  9545  dfacacn  9556  axdc2lem  9863  axcclem  9872  seqexw  13384  plusffval  17854  grpsubfval  18143  mulgfval  18222  staffval  19615  scaffval  19649  lpival  20015  ipffval  20341  nmfval  23199  tcphex  23825  tchnmfval  23836  orderseqlem  33208  rrnval  35264  lsatset  36285  fvnonrel  40294
  Copyright terms: Public domain W3C validator