Theorem comptiunov2i

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

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

Proof

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