Theorem fvssunirn 6698

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 6697	. . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅})
2		elssuni 4867	. . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})
4		uniun 4860	. . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅})
5		0ex 5210	. . . . 5 ⊢ ∅ ∈ V
6	5	unisn 4857	. . . 4 ⊢ ∪ {∅} = ∅
7	6	uneq2i 4135	. . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅)
8		un0 4343	. . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹
9	4, 7, 8	3eqtri 2848	. 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹
10	3, 9	sseqtri 4002	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ∈ wcel 2110   ∪ cun 3933   ⊆ wss 3935  ∅c0 4290  {csn 4566  ∪ cuni 4837  ran crn 5555  ‘cfv 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  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 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-cnv 5562  df-dm 5564  df-rn 5565  df-iota 6313  df-fv 6362

This theorem is referenced by:  ovssunirn  7191  marypha2lem1  8898  acnlem  9473  fin23lem29  9762  itunitc  9842  hsmexlem5  9851  wunfv  10153  wunex2  10159  strfvss  16505  prdsval  16727  prdsbas  16729  prdsplusg  16730  prdsmulr  16731  prdsvsca  16732  prdshom  16739  mreunirn  16871  mrcfval  16878  mrcssv  16884  mrisval  16900  sscpwex  17084  wunfunc  17168  catcxpccl  17456  comppfsc  22139  filunirn  22489  elflim  22578  flffval  22596  fclsval  22615  isfcls  22616  fcfval  22640  tsmsxplem1  22760  xmetunirn  22946  mopnval  23047  tmsval  23090  cfilfval  23866  caufval  23877  issgon  31382  elrnsiga  31385  volmeas  31490  omssubadd  31558  neibastop2lem  33708  ctbssinf  34686  ismtyval  35077  dicval  38311  ismrc  39296  nacsfix  39307  hbt  39728