Theorem fvssunirn 6803

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

Step	Hyp	Ref	Expression
1		fvrn0 6802	. . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅})
2		elssuni 4871	. . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})
4		uniun 4864	. . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅})
5		0ex 5231	. . . . 5 ⊢ ∅ ∈ V
6	5	unisn 4861	. . . 4 ⊢ ∪ {∅} = ∅
7	6	uneq2i 4094	. . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅)
8		un0 4324	. . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹
9	4, 7, 8	3eqtri 2770	. 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹
10	3, 9	sseqtri 3957	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ∈ wcel 2106   ∪ cun 3885   ⊆ wss 3887  ∅c0 4256  {csn 4561  ∪ cuni 4839  ran crn 5590  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600  df-iota 6391  df-fv 6441

This theorem is referenced by:  ovssunirn  7311  marypha2lem1  9194  acnlem  9804  fin23lem29  10097  itunitc  10177  hsmexlem5  10186  wunfv  10488  wunex2  10494  strfvss  16888  prdsvallem  17165  prdsval  17166  prdsbas  17168  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  prdshom  17178  mreunirn  17310  mrcfval  17317  mrcssv  17323  mrisval  17339  sscpwex  17527  wunfunc  17614  wunfuncOLD  17615  catcxpccl  17924  catcxpcclOLD  17925  comppfsc  22683  filunirn  23033  elflim  23122  flffval  23140  fclsval  23159  isfcls  23160  fcfval  23184  tsmsxplem1  23304  xmetunirn  23490  mopnval  23591  tmsval  23636  cfilfval  24428  caufval  24439  issgon  32091  elrnsiga  32094  volmeas  32199  omssubadd  32267  neibastop2lem  34549  ctbssinf  35577  ismtyval  35958  dicval  39190  ismrc  40523  nacsfix  40534  hbt  40955