Theorem fvssunirn 6204

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 6203	. . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅})
2		elssuni 4458	. . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})
4		uniun 4447	. . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅})
5		0ex 4781	. . . . 5 ⊢ ∅ ∈ V
6	5	unisn 4442	. . . 4 ⊢ ∪ {∅} = ∅
7	6	uneq2i 3756	. . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅)
8		un0 3958	. . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹
9	4, 7, 8	3eqtri 2646	. 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹
10	3, 9	sseqtri 3629	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ∈ wcel 1988   ∪ cun 3565   ⊆ wss 3567  ∅c0 3907  {csn 4168  ∪ cuni 4427  ran crn 5105  ‘cfv 5876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-cnv 5112  df-dm 5114  df-rn 5115  df-iota 5839  df-fv 5884

This theorem is referenced by:  ovssunirn  6666  marypha2lem1  8326  acnlem  8856  fin23lem29  9148  itunitc  9228  hsmexlem5  9237  wunfv  9539  wunex2  9545  strfvss  15861  prdsval  16096  prdsbas  16098  prdsplusg  16099  prdsmulr  16100  prdsvsca  16101  prdshom  16108  mreunirn  16242  mrcfval  16249  mrcssv  16255  mrisval  16271  sscpwex  16456  wunfunc  16540  catcxpccl  16828  comppfsc  21316  filunirn  21667  elflim  21756  flffval  21774  fclsval  21793  isfcls  21794  fcfval  21818  tsmsxplem1  21937  xmetunirn  22123  mopnval  22224  tmsval  22267  cfilfval  23043  caufval  23054  issgon  30160  elrnsiga  30163  volmeas  30268  omssubadd  30336  neibastop2lem  32330  ismtyval  33570  dicval  36284  ismrc  37083  nacsfix  37094  hbt  37519