Theorem fvssunirn 6358

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 6357	. . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅})
2		elssuni 4603	. . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})
4		uniun 4593	. . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅})
5		0ex 4924	. . . . 5 ⊢ ∅ ∈ V
6	5	unisn 4589	. . . 4 ⊢ ∪ {∅} = ∅
7	6	uneq2i 3915	. . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅)
8		un0 4111	. . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹
9	4, 7, 8	3eqtri 2797	. 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹
10	3, 9	sseqtri 3786	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ∈ wcel 2145   ∪ cun 3721   ⊆ wss 3723  ∅c0 4063  {csn 4316  ∪ cuni 4574  ran crn 5250  ‘cfv 6031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-cnv 5257  df-dm 5259  df-rn 5260  df-iota 5994  df-fv 6039

This theorem is referenced by:  ovssunirn  6826  marypha2lem1  8497  acnlem  9071  fin23lem29  9365  itunitc  9445  hsmexlem5  9454  wunfv  9756  wunex2  9762  strfvss  16087  prdsval  16323  prdsbas  16325  prdsplusg  16326  prdsmulr  16327  prdsvsca  16328  prdshom  16335  mreunirn  16469  mrcfval  16476  mrcssv  16482  mrisval  16498  sscpwex  16682  wunfunc  16766  catcxpccl  17055  comppfsc  21556  filunirn  21906  elflim  21995  flffval  22013  fclsval  22032  isfcls  22033  fcfval  22057  tsmsxplem1  22176  xmetunirn  22362  mopnval  22463  tmsval  22506  cfilfval  23281  caufval  23292  issgon  30526  elrnsiga  30529  volmeas  30634  omssubadd  30702  neibastop2lem  32692  ismtyval  33931  dicval  36986  ismrc  37790  nacsfix  37801  hbt  38226