Theorem comptiunov2i 44644

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 6568	. . 3 ⊢ Fun 𝑋
3		comptiunov2.y	. . . 4 ⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗))
4	3	funmpt2 6568	. . 3 ⊢ Fun 𝑌
5		funco 6569	. . 3 ⊢ ((Fun 𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌))
6	2, 4, 5	mp2an 705	. 2 ⊢ Fun (𝑋 ∘ 𝑌)
7		comptiunov2.z	. . 3 ⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘))
8	7	funmpt2 6568	. 2 ⊢ Fun 𝑍
9		ssv 3955	. . . . . . 7 ⊢ ran 𝑌 ⊆ V
10		comptiunov2.i	. . . . . . . . 9 ⊢ 𝐼 ∈ V
11		ovex 7442	. . . . . . . . 9 ⊢ (𝑎 ↑ 𝑖) ∈ V
12	10, 11	iunex 7964	. . . . . . . 8 ⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V
13	12, 1	dmmpti 6672	. . . . . . 7 ⊢ dom 𝑋 = V
14	9, 13	sseqtrri 3980	. . . . . 6 ⊢ ran 𝑌 ⊆ dom 𝑋
15		dmcosseq 5957	. . . . . 6 ⊢ (ran 𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌)
16	14, 15	ax-mp 5	. . . . 5 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑌
17		comptiunov2.j	. . . . . . 7 ⊢ 𝐽 ∈ V
18		ovex 7442	. . . . . . 7 ⊢ (𝑏 ↑ 𝑗) ∈ V
19	17, 18	iunex 7964	. . . . . 6 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V
20	19, 3	dmmpti 6672	. . . . 5 ⊢ dom 𝑌 = V
21	16, 20	eqtri 2783	. . . 4 ⊢ dom (𝑋 ∘ 𝑌) = V
22		comptiunov2.k	. . . . . . 7 ⊢ 𝐾 = (𝐼 ∪ 𝐽)
23	10, 17	unex 7745	. . . . . . 7 ⊢ (𝐼 ∪ 𝐽) ∈ V
24	22, 23	eqeltri 2856	. . . . . 6 ⊢ 𝐾 ∈ V
25		ovex 7442	. . . . . 6 ⊢ (𝑐 ↑ 𝑘) ∈ V
26	24, 25	iunex 7964	. . . . 5 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V
27	26, 7	dmmpti 6672	. . . 4 ⊢ dom 𝑍 = V
28	21, 27	eqtr4i 2786	. . 3 ⊢ dom (𝑋 ∘ 𝑌) = dom 𝑍
29		vex 3454	. . . . . . . . 9 ⊢ 𝑑 ∈ V
30	29, 20	eleqtrri 2859	. . . . . . . 8 ⊢ 𝑑 ∈ dom 𝑌
31		fvco 6972	. . . . . . . 8 ⊢ ((Fun 𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)))
32	4, 30, 31	mp2an 705	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))
33		oveq1 7416	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗))
34	33	iuneq2d 4981	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
35		ovex 7442	. . . . . . . . . . 11 ⊢ (𝑑 ↑ 𝑗) ∈ V
36	17, 35	iunex 7964	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V
37	34, 3, 36	fvmpt 6982	. . . . . . . . 9 ⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
38	37	elv 3455	. . . . . . . 8 ⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)
39	38	fveq2i 6877	. . . . . . 7 ⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗))
40		oveq1 7416	. . . . . . . . . 10 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
41	40	iuneq2d 4981	. . . . . . . . 9 ⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
42		ovex 7442	. . . . . . . . . 10 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
43	10, 42	iunex 7964	. . . . . . . . 9 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V
44	41, 1, 43	fvmpt 6982	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖))
45	36, 44	ax-mp 5	. . . . . . 7 ⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
46	32, 39, 45	3eqtri 2787	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
47		oveq1 7416	. . . . . . . . 9 ⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘))
48	47	iuneq2d 4981	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
49		ovex 7442	. . . . . . . . 9 ⊢ (𝑑 ↑ 𝑘) ∈ V
50	24, 49	iunex 7964	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V
51	48, 7, 50	fvmpt 6982	. . . . . . 7 ⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
52	51	elv 3455	. . . . . 6 ⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
53	46, 52	eqeq12i 2778	. . . . 5 ⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
54	21, 53	raleqbii 3332	. . . 4 ⊢ (∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∀𝑑 ∈ V ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
55		comptiunov2.3	. . . . . . 7 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
56		iunxun 5054	. . . . . . . 8 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) = (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘))
57		comptiunov2.1	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
58		comptiunov2.2	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
59	57, 58	unssi 4137	. . . . . . . 8 ⊢ (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
60	56, 59	eqsstri 3977	. . . . . . 7 ⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)
61	55, 60	eqssi 3947	. . . . . 6 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
62		iuneq1 4968	. . . . . . 7 ⊢ (𝐾 = (𝐼 ∪ 𝐽) → ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘))
63	22, 62	ax-mp 5	. . . . . 6 ⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)
64	61, 63	eqtr4i 2786	. . . . 5 ⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)
65	64	a1i 11	. . . 4 ⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘))
66	54, 65	mprgbir 3083	. . 3 ⊢ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)
67		eqfunfv 7024	. . . 4 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑))))
68	67	biimprd 251	. . 3 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍))
69	28, 66, 68	mp2ani 711	. 2 ⊢ ((Fun (𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍)
70	6, 8, 69	mp2an 705	1 ⊢ (𝑋 ∘ 𝑌) = 𝑍

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  Vcvv 3450   ∪ cun 3897   ⊆ wss 3899  ∪ ciun 4951   ↦ cmpt 5186  dom cdm 5648  ran crn 5649   ∘ ccom 5652  Fun wfun 6522  ‘cfv 6528  (class class class)co 7409

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-fv 6536  df-ov 7412

This theorem is used by:  corclrcl  44645  cotrcltrcl  44663  corcltrcl  44677  cotrclrcl  44680