Theorem funiunfv 7240

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 6578	. . . 4 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
2	1	funfnd 6567	. . 3 ⊢ (Fun 𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴))
3		fniunfv 7239	. . 3 ⊢ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴))
4	2, 3	syl 17	. 2 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴))
5		undif2 4452	. . . . 5 ⊢ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = (dom (𝐹 ↾ 𝐴) ∪ 𝐴)
6		dmres 5999	. . . . . . 7 ⊢ dom (𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹)
7		inss1 4212	. . . . . . 7 ⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴
8	6, 7	eqsstri 4005	. . . . . 6 ⊢ dom (𝐹 ↾ 𝐴) ⊆ 𝐴
9		ssequn1 4161	. . . . . 6 ⊢ (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴)
10	8, 9	mpbi 230	. . . . 5 ⊢ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴
11	5, 10	eqtri 2758	. . . 4 ⊢ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴
12		iuneq1 4984	. . . 4 ⊢ ((dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 → ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥))
13	11, 12	ax-mp 5	. . 3 ⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥)
14		iunxun 5070	. . . 4 ⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥))
15		eldifn 4107	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴))
16		ndmfv 6911	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅)
17	15, 16	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅)
18	17	iuneq2i 4989	. . . . . . 7 ⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅
19		iun0 5038	. . . . . . 7 ⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ = ∅
20	18, 19	eqtri 2758	. . . . . 6 ⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∅
21	20	uneq2i 4140	. . . . 5 ⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅)
22		un0 4369	. . . . 5 ⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
23	21, 22	eqtri 2758	. . . 4 ⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
24	14, 23	eqtri 2758	. . 3 ⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
25		fvres 6895	. . . 4 ⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥))
26	25	iuneq2i 4989	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)
27	13, 24, 26	3eqtr3ri 2767	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥)
28		df-ima 5667	. . 3 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
29	28	unieqi 4895	. 2 ⊢ ∪ (𝐹 “ 𝐴) = ∪ ran (𝐹 ↾ 𝐴)
30	4, 27, 29	3eqtr4g 2795	1 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925   ⊆ wss 3926  ∅c0 4308  ∪ cuni 4883  ∪ ciun 4967  dom cdm 5654  ran crn 5655   ↾ cres 5656   “ cima 5657  Fun wfun 6525   Fn wfn 6526  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is referenced by:  funiunfvf  7241  eluniima  7242  marypha2lem4  9450  r1limg  9785  r1elssi  9819  r1elss  9820  ackbij2  10256  r1om  10257  ttukeylem6  10528  isacs2  17665  mreacs  17670  acsfn  17671  isacs5  18558  dprdss  20012  dprd2dlem1  20024  dmdprdsplit2lem  20028  uniioombllem3a  25537  uniioombllem4  25539  uniioombllem5  25540  dyadmbl  25553  oldlim  27850  precsexlem10  28170  precsexlem11  28171  mblfinlem1  37681  ovoliunnfl  37686  voliunnfl  37688  uniimafveqt  47395  imasetpreimafvbijlemfv  47416