Theorem comptiunov2i 42443

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 6585	. . 3 ⊢ Fun 𝑋
3		comptiunov2.y	. . . 4 ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))
4	3	funmpt2 6585	. . 3 ⊢ Fun 𝑌
5		funco 6586	. . 3 ⊢ ((Fun 𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌))
6	2, 4, 5	mp2an 691	. 2 ⊢ Fun (𝑋 ∘ 𝑌)
7		comptiunov2.z	. . 3 ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))
8	7	funmpt2 6585	. 2 ⊢ Fun 𝑍
9		ssv 4006	. . . . . . 7 ⊢ ran 𝑌 ⊆ V
10		comptiunov2.i	. . . . . . . . 9 ⊢ 𝐼 ∈ V
11		ovex 7439	. . . . . . . . 9 ⊢ (𝑎 ↑ 𝑖) ∈ V
12	10, 11	iunex 7952	. . . . . . . 8 ⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V
13	12, 1	dmmpti 6692	. . . . . . 7 ⊢ dom 𝑋 = V
14	9, 13	sseqtrri 4019	. . . . . 6 ⊢ ran 𝑌 ⊆ dom 𝑋
15		dmcosseq 5971	. . . . . 6 ⊢ (ran 𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌)
16	14, 15	ax-mp 5	. . . . 5 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑌
17		comptiunov2.j	. . . . . . 7 ⊢ 𝐽 ∈ V
18		ovex 7439	. . . . . . 7 ⊢ (𝑏 ↑ 𝑗) ∈ V
19	17, 18	iunex 7952	. . . . . 6 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V
20	19, 3	dmmpti 6692	. . . . 5 ⊢ dom 𝑌 = V
21	16, 20	eqtri 2761	. . . 4 ⊢ dom (𝑋 ∘ 𝑌) = V
22		comptiunov2.k	. . . . . . 7 ⊢ 𝐾 = (𝐼 ∪ 𝐽)
23	10, 17	unex 7730	. . . . . . 7 ⊢ (𝐼 ∪ 𝐽) ∈ V
24	22, 23	eqeltri 2830	. . . . . 6 ⊢ 𝐾 ∈ V
25		ovex 7439	. . . . . 6 ⊢ (𝑐 ↑ 𝑘) ∈ V
26	24, 25	iunex 7952	. . . . 5 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V
27	26, 7	dmmpti 6692	. . . 4 ⊢ dom 𝑍 = V
28	21, 27	eqtr4i 2764	. . 3 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑍
29		vex 3479	. . . . . . . . 9 ⊢ 𝑑 ∈ V
30	29, 20	eleqtrri 2833	. . . . . . . 8 ⊢ 𝑑 ∈ dom 𝑌
31		fvco 6987	. . . . . . . 8 ⊢ ((Fun 𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)))
32	4, 30, 31	mp2an 691	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))
33		oveq1 7413	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗))
34	33	iuneq2d 5026	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
35		ovex 7439	. . . . . . . . . . 11 ⊢ (𝑑 ↑ 𝑗) ∈ V
36	17, 35	iunex 7952	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V
37	34, 3, 36	fvmpt 6996	. . . . . . . . 9 ⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
38	37	elv 3481	. . . . . . . 8 ⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)
39	38	fveq2i 6892	. . . . . . 7 ⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
40		oveq1 7413	. . . . . . . . . 10 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
41	40	iuneq2d 5026	. . . . . . . . 9 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
42		ovex 7439	. . . . . . . . . 10 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
43	10, 42	iunex 7952	. . . . . . . . 9 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
44	41, 1, 43	fvmpt 6996	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
45	36, 44	ax-mp 5	. . . . . . 7 ⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
46	32, 39, 45	3eqtri 2765	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
47		oveq1 7413	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘))
48	47	iuneq2d 5026	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
49		ovex 7439	. . . . . . . . 9 ⊢ (𝑑 ↑ 𝑘) ∈ V
50	24, 49	iunex 7952	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V
51	48, 7, 50	fvmpt 6996	. . . . . . 7 ⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
52	51	elv 3481	. . . . . 6 ⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
53	46, 52	eqeq12i 2751	. . . . 5 ⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
54	21, 53	raleqbii 3339	. . . 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 2764	. . . . 5 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
65	64	a1i 11	. . . 4 ⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
66	54, 65	mprgbir 3069	. . 3 ⊢ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)
67		eqfunfv 7035	. . . 4 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑))))
68	67	biimprd 247	. . 3 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍))
69	28, 66, 68	mp2ani 697	. 2 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍)
70	6, 8, 69	mp2an 691	1 ⊢ (𝑋 ∘ 𝑌) = 𝑍

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   ∪ cun 3946   ⊆ wss 3948  ∪ ciun 4997   ↦ cmpt 5231  dom cdm 5676  ran crn 5677   ∘ ccom 5680  Fun wfun 6535  ‘cfv 6541  (class class class)co 7406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  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 6493  df-fun 6543  df-fn 6544  df-fv 6549  df-ov 7409

This theorem is referenced by:  corclrcl  42444  cotrcltrcl  42462  corcltrcl  42476  cotrclrcl  42479