Theorem funiunfv 7191

Description: The indexed union of a function's values is the union of its image under the index class.

Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to 𝐹 Fn 𝐴, the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
funiunfv	⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem funiunfv

Step	Hyp	Ref	Expression
1		funres 6531	. . . 4 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
2	1	funfnd 6520	. . 3 ⊢ (Fun 𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴))
3		fniunfv 7190	. . 3 ⊢ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴))
4	2, 3	syl 17	. 2 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴))
5		undif2 4428	. . . . 5 ⊢ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = (dom (𝐹 ↾ 𝐴) ∪ 𝐴)
6		dmres 5968	. . . . . . 7 ⊢ dom (𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹)
7		inss1 4188	. . . . . . 7 ⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴
8	6, 7	eqsstri 3978	. . . . . 6 ⊢ dom (𝐹 ↾ 𝐴) ⊆ 𝐴
9		ssequn1 4137	. . . . . 6 ⊢ (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴)
10	8, 9	mpbi 230	. . . . 5 ⊢ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴
11	5, 10	eqtri 2756	. . . 4 ⊢ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴
12		iuneq1 4960	. . . 4 ⊢ ((dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 → ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥))
13	11, 12	ax-mp 5	. . 3 ⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥)
14		iunxun 5046	. . . 4 ⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥))
15		eldifn 4083	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴))
16		ndmfv 6863	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅)
17	15, 16	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅)
18	17	iuneq2i 4965	. . . . . . 7 ⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅
19		iun0 5014	. . . . . . 7 ⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ = ∅
20	18, 19	eqtri 2756	. . . . . 6 ⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∅
21	20	uneq2i 4116	. . . . 5 ⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅)
22		un0 4345	. . . . 5 ⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
23	21, 22	eqtri 2756	. . . 4 ⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
24	14, 23	eqtri 2756	. . 3 ⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
25		fvres 6850	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥))
26	25	iuneq2i 4965	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)
27	13, 24, 26	3eqtr3ri 2765	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
28		df-ima 5634	. . 3 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
29	28	unieqi 4872	. 2 ⊢ ∪ (𝐹 “ 𝐴) = ∪ ran (𝐹 ↾ 𝐴)
30	4, 27, 29	3eqtr4g 2793	1 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4284  ∪ cuni 4860  ∪ ciun 4943  dom cdm 5621  ran crn 5622   ↾ cres 5623   “ cima 5624  Fun wfun 6483   Fn wfn 6484  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  funiunfvf  7192  eluniima  7193  marypha2lem4  9332  r1limg  9674  r1elssi  9708  r1elss  9709  ackbij2  10143  r1om  10144  ttukeylem6  10415  isacs2  17569  mreacs  17574  acsfn  17575  isacs5  18464  dprdss  19953  dprd2dlem1  19965  dmdprdsplit2lem  19969  uniioombllem3a  25522  uniioombllem4  25524  uniioombllem5  25525  dyadmbl  25538  oldlim  27842  precsexlem10  28164  precsexlem11  28165  r1omfv  35132  mblfinlem1  37707  ovoliunnfl  37712  voliunnfl  37714  uniimafveqt  47495  imasetpreimafvbijlemfv  47516