Theorem comptiunov2i 42919

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 6587	. . 3 ⊢ Fun 𝑋
3		comptiunov2.y	. . . 4 ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))
4	3	funmpt2 6587	. . 3 ⊢ Fun 𝑌
5		funco 6588	. . 3 ⊢ ((Fun 𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌))
6	2, 4, 5	mp2an 689	. 2 ⊢ Fun (𝑋 ∘ 𝑌)
7		comptiunov2.z	. . 3 ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))
8	7	funmpt2 6587	. 2 ⊢ Fun 𝑍
9		ssv 4006	. . . . . . 7 ⊢ ran 𝑌 ⊆ V
10		comptiunov2.i	. . . . . . . . 9 ⊢ 𝐼 ∈ V
11		ovex 7445	. . . . . . . . 9 ⊢ (𝑎 ↑ 𝑖) ∈ V
12	10, 11	iunex 7959	. . . . . . . 8 ⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V
13	12, 1	dmmpti 6694	. . . . . . 7 ⊢ dom 𝑋 = V
14	9, 13	sseqtrri 4019	. . . . . 6 ⊢ ran 𝑌 ⊆ dom 𝑋
15		dmcosseq 5972	. . . . . 6 ⊢ (ran 𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌)
16	14, 15	ax-mp 5	. . . . 5 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑌
17		comptiunov2.j	. . . . . . 7 ⊢ 𝐽 ∈ V
18		ovex 7445	. . . . . . 7 ⊢ (𝑏 ↑ 𝑗) ∈ V
19	17, 18	iunex 7959	. . . . . 6 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V
20	19, 3	dmmpti 6694	. . . . 5 ⊢ dom 𝑌 = V
21	16, 20	eqtri 2759	. . . 4 ⊢ dom (𝑋 ∘ 𝑌) = V
22		comptiunov2.k	. . . . . . 7 ⊢ 𝐾 = (𝐼 ∪ 𝐽)
23	10, 17	unex 7737	. . . . . . 7 ⊢ (𝐼 ∪ 𝐽) ∈ V
24	22, 23	eqeltri 2828	. . . . . 6 ⊢ 𝐾 ∈ V
25		ovex 7445	. . . . . 6 ⊢ (𝑐 ↑ 𝑘) ∈ V
26	24, 25	iunex 7959	. . . . 5 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V
27	26, 7	dmmpti 6694	. . . 4 ⊢ dom 𝑍 = V
28	21, 27	eqtr4i 2762	. . 3 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑍
29		vex 3477	. . . . . . . . 9 ⊢ 𝑑 ∈ V
30	29, 20	eleqtrri 2831	. . . . . . . 8 ⊢ 𝑑 ∈ dom 𝑌
31		fvco 6989	. . . . . . . 8 ⊢ ((Fun 𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)))
32	4, 30, 31	mp2an 689	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))
33		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗))
34	33	iuneq2d 5026	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
35		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑑 ↑ 𝑗) ∈ V
36	17, 35	iunex 7959	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V
37	34, 3, 36	fvmpt 6998	. . . . . . . . 9 ⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
38	37	elv 3479	. . . . . . . 8 ⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)
39	38	fveq2i 6894	. . . . . . 7 ⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
40		oveq1 7419	. . . . . . . . . 10 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
41	40	iuneq2d 5026	. . . . . . . . 9 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
42		ovex 7445	. . . . . . . . . 10 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
43	10, 42	iunex 7959	. . . . . . . . 9 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
44	41, 1, 43	fvmpt 6998	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
45	36, 44	ax-mp 5	. . . . . . 7 ⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
46	32, 39, 45	3eqtri 2763	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
47		oveq1 7419	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘))
48	47	iuneq2d 5026	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
49		ovex 7445	. . . . . . . . 9 ⊢ (𝑑 ↑ 𝑘) ∈ V
50	24, 49	iunex 7959	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V
51	48, 7, 50	fvmpt 6998	. . . . . . 7 ⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
52	51	elv 3479	. . . . . 6 ⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
53	46, 52	eqeq12i 2749	. . . . 5 ⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
54	21, 53	raleqbii 3337	. . . 4 ⊢ (∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∀𝑑 ∈ V ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
55		comptiunov2.3	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
56		iunxun 5097	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) = (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘))
57		comptiunov2.1	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
58		comptiunov2.2	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
59	57, 58	unssi 4185	. . . . . . . 8 ⊢ (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
60	56, 59	eqsstri 4016	. . . . . . 7 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
61	55, 60	eqssi 3998	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
62		iuneq1 5013	. . . . . . 7 ⊢ (𝐾 = (𝐼 ∪ 𝐽) → ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘))
63	22, 62	ax-mp 5	. . . . . 6 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
64	61, 63	eqtr4i 2762	. . . . 5 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
65	64	a1i 11	. . . 4 ⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
66	54, 65	mprgbir 3067	. . 3 ⊢ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)
67		eqfunfv 7037	. . . 4 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑))))
68	67	biimprd 247	. . 3 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍))
69	28, 66, 68	mp2ani 695	. 2 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍)
70	6, 8, 69	mp2an 689	1 ⊢ (𝑋 ∘ 𝑌) = 𝑍

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2105  ∀wral 3060  Vcvv 3473   ∪ cun 3946   ⊆ wss 3948  ∪ ciun 4997   ↦ cmpt 5231  dom cdm 5676  ran crn 5677   ∘ ccom 5680  Fun wfun 6537  ‘cfv 6543  (class class class)co 7412

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551  df-ov 7415

This theorem is referenced by:  corclrcl  42920  cotrcltrcl  42938  corcltrcl  42952  cotrclrcl  42955