Theorem comptiunov2i 41968

Description: The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.)

Hypotheses

Ref	Expression
comptiunov2.x	⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖))
comptiunov2.y	⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))
comptiunov2.z	⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))
comptiunov2.i	⊢ 𝐼 ∈ V
comptiunov2.j	⊢ 𝐽 ∈ V
comptiunov2.k	⊢ 𝐾 = (𝐼 ∪ 𝐽)
comptiunov2.1	⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
comptiunov2.2	⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
comptiunov2.3	⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)

Assertion

Ref	Expression
comptiunov2i	⊢ (𝑋 ∘ 𝑌) = 𝑍

Distinct variable groups:   𝑖,𝑎, ↑   ↑ ,𝑏   ↑ ,𝑐   𝐼,𝑎,𝑖   𝑘,𝐼   𝑗,𝑎,𝐽,𝑖   𝐽,𝑏   𝑘,𝐽   𝑘,𝑐,𝐾   𝑋,𝑑   𝑌,𝑑   𝑍,𝑑   𝑎,𝑑,𝑖,𝑗   𝑏,𝑑,𝑗   𝑐,𝑑,𝑘

Allowed substitution hints:   ↑ (𝑗,𝑘,𝑑)   𝐼(𝑗,𝑏,𝑐,𝑑)   𝐽(𝑐,𝑑)   𝐾(𝑖,𝑗,𝑎,𝑏,𝑑)   𝑋(𝑖,𝑗,𝑘,𝑎,𝑏,𝑐)   𝑌(𝑖,𝑗,𝑘,𝑎,𝑏,𝑐)   𝑍(𝑖,𝑗,𝑘,𝑎,𝑏,𝑐)

Proof of Theorem comptiunov2i

Step	Hyp	Ref	Expression
1		comptiunov2.x	. . . 4 ⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖))
2	1	funmpt2 6540	. . 3 ⊢ Fun 𝑋
3		comptiunov2.y	. . . 4 ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))
4	3	funmpt2 6540	. . 3 ⊢ Fun 𝑌
5		funco 6541	. . 3 ⊢ ((Fun 𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌))
6	2, 4, 5	mp2an 690	. 2 ⊢ Fun (𝑋 ∘ 𝑌)
7		comptiunov2.z	. . 3 ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))
8	7	funmpt2 6540	. 2 ⊢ Fun 𝑍
9		ssv 3968	. . . . . . 7 ⊢ ran 𝑌 ⊆ V
10		comptiunov2.i	. . . . . . . . 9 ⊢ 𝐼 ∈ V
11		ovex 7390	. . . . . . . . 9 ⊢ (𝑎 ↑ 𝑖) ∈ V
12	10, 11	iunex 7901	. . . . . . . 8 ⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V
13	12, 1	dmmpti 6645	. . . . . . 7 ⊢ dom 𝑋 = V
14	9, 13	sseqtrri 3981	. . . . . 6 ⊢ ran 𝑌 ⊆ dom 𝑋
15		dmcosseq 5928	. . . . . 6 ⊢ (ran 𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌)
16	14, 15	ax-mp 5	. . . . 5 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑌
17		comptiunov2.j	. . . . . . 7 ⊢ 𝐽 ∈ V
18		ovex 7390	. . . . . . 7 ⊢ (𝑏 ↑ 𝑗) ∈ V
19	17, 18	iunex 7901	. . . . . 6 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V
20	19, 3	dmmpti 6645	. . . . 5 ⊢ dom 𝑌 = V
21	16, 20	eqtri 2764	. . . 4 ⊢ dom (𝑋 ∘ 𝑌) = V
22		comptiunov2.k	. . . . . . 7 ⊢ 𝐾 = (𝐼 ∪ 𝐽)
23	10, 17	unex 7680	. . . . . . 7 ⊢ (𝐼 ∪ 𝐽) ∈ V
24	22, 23	eqeltri 2834	. . . . . 6 ⊢ 𝐾 ∈ V
25		ovex 7390	. . . . . 6 ⊢ (𝑐 ↑ 𝑘) ∈ V
26	24, 25	iunex 7901	. . . . 5 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V
27	26, 7	dmmpti 6645	. . . 4 ⊢ dom 𝑍 = V
28	21, 27	eqtr4i 2767	. . 3 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑍
29		vex 3449	. . . . . . . . 9 ⊢ 𝑑 ∈ V
30	29, 20	eleqtrri 2837	. . . . . . . 8 ⊢ 𝑑 ∈ dom 𝑌
31		fvco 6939	. . . . . . . 8 ⊢ ((Fun 𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)))
32	4, 30, 31	mp2an 690	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))
33		oveq1 7364	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗))
34	33	iuneq2d 4983	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
35		ovex 7390	. . . . . . . . . . 11 ⊢ (𝑑 ↑ 𝑗) ∈ V
36	17, 35	iunex 7901	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V
37	34, 3, 36	fvmpt 6948	. . . . . . . . 9 ⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
38	37	elv 3451	. . . . . . . 8 ⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)
39	38	fveq2i 6845	. . . . . . 7 ⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
40		oveq1 7364	. . . . . . . . . 10 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
41	40	iuneq2d 4983	. . . . . . . . 9 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
42		ovex 7390	. . . . . . . . . 10 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
43	10, 42	iunex 7901	. . . . . . . . 9 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
44	41, 1, 43	fvmpt 6948	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
45	36, 44	ax-mp 5	. . . . . . 7 ⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
46	32, 39, 45	3eqtri 2768	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
47		oveq1 7364	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘))
48	47	iuneq2d 4983	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
49		ovex 7390	. . . . . . . . 9 ⊢ (𝑑 ↑ 𝑘) ∈ V
50	24, 49	iunex 7901	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V
51	48, 7, 50	fvmpt 6948	. . . . . . 7 ⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
52	51	elv 3451	. . . . . 6 ⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
53	46, 52	eqeq12i 2754	. . . . 5 ⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
54	21, 53	raleqbii 3315	. . . 4 ⊢ (∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∀𝑑 ∈ V ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
55		comptiunov2.3	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
56		iunxun 5054	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) = (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘))
57		comptiunov2.1	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
58		comptiunov2.2	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
59	57, 58	unssi 4145	. . . . . . . 8 ⊢ (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
60	56, 59	eqsstri 3978	. . . . . . 7 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
61	55, 60	eqssi 3960	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
62		iuneq1 4970	. . . . . . 7 ⊢ (𝐾 = (𝐼 ∪ 𝐽) → ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘))
63	22, 62	ax-mp 5	. . . . . 6 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
64	61, 63	eqtr4i 2767	. . . . 5 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
65	64	a1i 11	. . . 4 ⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
66	54, 65	mprgbir 3071	. . 3 ⊢ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)
67		eqfunfv 6987	. . . 4 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑))))
68	67	biimprd 247	. . 3 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍))
69	28, 66, 68	mp2ani 696	. 2 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍)
70	6, 8, 69	mp2an 690	1 ⊢ (𝑋 ∘ 𝑌) = 𝑍

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3064  Vcvv 3445   ∪ cun 3908   ⊆ wss 3910  ∪ ciun 4954   ↦ cmpt 5188  dom cdm 5633  ran crn 5634   ∘ ccom 5637  Fun wfun 6490  ‘cfv 6496  (class class class)co 7357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-fv 6504  df-ov 7360

This theorem is referenced by:  corclrcl  41969  cotrcltrcl  41987  corcltrcl  42001  cotrclrcl  42004