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

Theorem fvssunirn 6693
Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
fvssunirn (𝐹𝑋) ⊆ ran 𝐹

Proof of Theorem fvssunirn
StepHypRef Expression
1 fvrn0 6692 . . 3 (𝐹𝑋) ∈ (ran 𝐹 ∪ {∅})
2 elssuni 4861 . . 3 ((𝐹𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑋) ⊆ (ran 𝐹 ∪ {∅}))
31, 2ax-mp 5 . 2 (𝐹𝑋) ⊆ (ran 𝐹 ∪ {∅})
4 uniun 4851 . . 3 (ran 𝐹 ∪ {∅}) = ( ran 𝐹 {∅})
5 0ex 5203 . . . . 5 ∅ ∈ V
65unisn 4848 . . . 4 {∅} = ∅
76uneq2i 4135 . . 3 ( ran 𝐹 {∅}) = ( ran 𝐹 ∪ ∅)
8 un0 4343 . . 3 ( ran 𝐹 ∪ ∅) = ran 𝐹
94, 7, 83eqtri 2848 . 2 (ran 𝐹 ∪ {∅}) = ran 𝐹
103, 9sseqtri 4002 1 (𝐹𝑋) ⊆ ran 𝐹
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  cun 3933  wss 3935  c0 4290  {csn 4559   cuni 4832  ran crn 5550  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-cnv 5557  df-dm 5559  df-rn 5560  df-iota 6308  df-fv 6357
This theorem is referenced by:  ovssunirn  7181  marypha2lem1  8888  acnlem  9463  fin23lem29  9752  itunitc  9832  hsmexlem5  9841  wunfv  10143  wunex2  10149  strfvss  16496  prdsval  16718  prdsbas  16720  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  prdshom  16730  mreunirn  16862  mrcfval  16869  mrcssv  16875  mrisval  16891  sscpwex  17075  wunfunc  17159  catcxpccl  17447  comppfsc  22070  filunirn  22420  elflim  22509  flffval  22527  fclsval  22546  isfcls  22547  fcfval  22571  tsmsxplem1  22690  xmetunirn  22876  mopnval  22977  tmsval  23020  cfilfval  23796  caufval  23807  issgon  31282  elrnsiga  31285  volmeas  31390  omssubadd  31458  neibastop2lem  33606  ctbssinf  34570  ismtyval  34961  dicval  38194  ismrc  39178  nacsfix  39189  hbt  39610
  Copyright terms: Public domain W3C validator