Theorem fvssunirn 6477

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 6476	. . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅})
2		elssuni 4704	. . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})
4		uniun 4694	. . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅})
5		0ex 5028	. . . . 5 ⊢ ∅ ∈ V
6	5	unisn 4689	. . . 4 ⊢ ∪ {∅} = ∅
7	6	uneq2i 3987	. . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅)
8		un0 4193	. . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹
9	4, 7, 8	3eqtri 2806	. 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹
10	3, 9	sseqtri 3856	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ∈ wcel 2107   ∪ cun 3790   ⊆ wss 3792  ∅c0 4141  {csn 4398  ∪ cuni 4673  ran crn 5358  ‘cfv 6137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-cnv 5365  df-dm 5367  df-rn 5368  df-iota 6101  df-fv 6145

This theorem is referenced by:  ovssunirn  6959  marypha2lem1  8631  acnlem  9206  fin23lem29  9500  itunitc  9580  hsmexlem5  9589  wunfv  9891  wunex2  9897  strfvss  16289  prdsval  16512  prdsbas  16514  prdsplusg  16515  prdsmulr  16516  prdsvsca  16517  prdshom  16524  mreunirn  16658  mrcfval  16665  mrcssv  16671  mrisval  16687  sscpwex  16871  wunfunc  16955  catcxpccl  17244  comppfsc  21755  filunirn  22105  elflim  22194  flffval  22212  fclsval  22231  isfcls  22232  fcfval  22256  tsmsxplem1  22375  xmetunirn  22561  mopnval  22662  tmsval  22705  cfilfval  23481  caufval  23492  issgon  30792  elrnsiga  30795  volmeas  30900  omssubadd  30968  neibastop2lem  32951  ismtyval  34232  dicval  37339  ismrc  38238  nacsfix  38249  hbt  38673