Theorem comptiunov2i 43702

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 6558	. . 3 ⊢ Fun 𝑋
3		comptiunov2.y	. . . 4 ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))
4	3	funmpt2 6558	. . 3 ⊢ Fun 𝑌
5		funco 6559	. . 3 ⊢ ((Fun 𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌))
6	2, 4, 5	mp2an 692	. 2 ⊢ Fun (𝑋 ∘ 𝑌)
7		comptiunov2.z	. . 3 ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))
8	7	funmpt2 6558	. 2 ⊢ Fun 𝑍
9		ssv 3974	. . . . . . 7 ⊢ ran 𝑌 ⊆ V
10		comptiunov2.i	. . . . . . . . 9 ⊢ 𝐼 ∈ V
11		ovex 7423	. . . . . . . . 9 ⊢ (𝑎 ↑ 𝑖) ∈ V
12	10, 11	iunex 7950	. . . . . . . 8 ⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V
13	12, 1	dmmpti 6665	. . . . . . 7 ⊢ dom 𝑋 = V
14	9, 13	sseqtrri 3999	. . . . . 6 ⊢ ran 𝑌 ⊆ dom 𝑋
15		dmcosseq 5943	. . . . . 6 ⊢ (ran 𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌)
16	14, 15	ax-mp 5	. . . . 5 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑌
17		comptiunov2.j	. . . . . . 7 ⊢ 𝐽 ∈ V
18		ovex 7423	. . . . . . 7 ⊢ (𝑏 ↑ 𝑗) ∈ V
19	17, 18	iunex 7950	. . . . . 6 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V
20	19, 3	dmmpti 6665	. . . . 5 ⊢ dom 𝑌 = V
21	16, 20	eqtri 2753	. . . 4 ⊢ dom (𝑋 ∘ 𝑌) = V
22		comptiunov2.k	. . . . . . 7 ⊢ 𝐾 = (𝐼 ∪ 𝐽)
23	10, 17	unex 7723	. . . . . . 7 ⊢ (𝐼 ∪ 𝐽) ∈ V
24	22, 23	eqeltri 2825	. . . . . 6 ⊢ 𝐾 ∈ V
25		ovex 7423	. . . . . 6 ⊢ (𝑐 ↑ 𝑘) ∈ V
26	24, 25	iunex 7950	. . . . 5 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V
27	26, 7	dmmpti 6665	. . . 4 ⊢ dom 𝑍 = V
28	21, 27	eqtr4i 2756	. . 3 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑍
29		vex 3454	. . . . . . . . 9 ⊢ 𝑑 ∈ V
30	29, 20	eleqtrri 2828	. . . . . . . 8 ⊢ 𝑑 ∈ dom 𝑌
31		fvco 6962	. . . . . . . 8 ⊢ ((Fun 𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)))
32	4, 30, 31	mp2an 692	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))
33		oveq1 7397	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗))
34	33	iuneq2d 4989	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
35		ovex 7423	. . . . . . . . . . 11 ⊢ (𝑑 ↑ 𝑗) ∈ V
36	17, 35	iunex 7950	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V
37	34, 3, 36	fvmpt 6971	. . . . . . . . 9 ⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
38	37	elv 3455	. . . . . . . 8 ⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)
39	38	fveq2i 6864	. . . . . . 7 ⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
40		oveq1 7397	. . . . . . . . . 10 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
41	40	iuneq2d 4989	. . . . . . . . 9 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
42		ovex 7423	. . . . . . . . . 10 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
43	10, 42	iunex 7950	. . . . . . . . 9 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
44	41, 1, 43	fvmpt 6971	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
45	36, 44	ax-mp 5	. . . . . . 7 ⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
46	32, 39, 45	3eqtri 2757	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
47		oveq1 7397	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘))
48	47	iuneq2d 4989	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
49		ovex 7423	. . . . . . . . 9 ⊢ (𝑑 ↑ 𝑘) ∈ V
50	24, 49	iunex 7950	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V
51	48, 7, 50	fvmpt 6971	. . . . . . 7 ⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
52	51	elv 3455	. . . . . 6 ⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
53	46, 52	eqeq12i 2748	. . . . 5 ⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
54	21, 53	raleqbii 3319	. . . 4 ⊢ (∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∀𝑑 ∈ V ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
55		comptiunov2.3	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
56		iunxun 5061	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) = (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘))
57		comptiunov2.1	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
58		comptiunov2.2	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
59	57, 58	unssi 4157	. . . . . . . 8 ⊢ (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
60	56, 59	eqsstri 3996	. . . . . . 7 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
61	55, 60	eqssi 3966	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
62		iuneq1 4975	. . . . . . 7 ⊢ (𝐾 = (𝐼 ∪ 𝐽) → ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘))
63	22, 62	ax-mp 5	. . . . . 6 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
64	61, 63	eqtr4i 2756	. . . . 5 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
65	64	a1i 11	. . . 4 ⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
66	54, 65	mprgbir 3052	. . 3 ⊢ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)
67		eqfunfv 7011	. . . 4 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑))))
68	67	biimprd 248	. . 3 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍))
69	28, 66, 68	mp2ani 698	. 2 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍)
70	6, 8, 69	mp2an 692	1 ⊢ (𝑋 ∘ 𝑌) = 𝑍

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  ∪ ciun 4958   ↦ cmpt 5191  dom cdm 5641  ran crn 5642   ∘ ccom 5645  Fun wfun 6508  ‘cfv 6514  (class class class)co 7390

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522  df-ov 7393

This theorem is referenced by:  corclrcl  43703  cotrcltrcl  43721  corcltrcl  43735  cotrclrcl  43738