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	$$⊢X=\left(a\in \mathrm{V}⟼\bigcup _{i\in I}\left(a\underset{\dot{}}{\times }i\right)\right)$$
	comptiunov2.y	$$⊢Y=\left(b\in \mathrm{V}⟼\bigcup _{j\in J}\left(b\underset{\dot{}}{\times }j\right)\right)$$
	comptiunov2.z	$$⊢Z=\left(c\in \mathrm{V}⟼\bigcup _{k\in K}\left(c\underset{\dot{}}{\times }k\right)\right)$$
	comptiunov2.i	$$⊢I\in \mathrm{V}$$
	comptiunov2.j	$$⊢J\in \mathrm{V}$$
	comptiunov2.k	$$⊢K=I\cup J$$
	comptiunov2.1	$$⊢\bigcup _{k\in I}\left(d\underset{\dot{}}{\times }k\right)\subseteq \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
	comptiunov2.2	$$⊢\bigcup _{k\in J}\left(d\underset{\dot{}}{\times }k\right)\subseteq \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
	comptiunov2.3	$$⊢\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)\subseteq \bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)$$
Assertion	comptiunov2i	$$⊢X\circ Y=Z$$

Proof

Step	Hyp	Ref	Expression
1		comptiunov2.x	$$⊢X=\left(a\in \mathrm{V}⟼\bigcup _{i\in I}\left(a\underset{\dot{}}{\times }i\right)\right)$$
2		comptiunov2.y	$$⊢Y=\left(b\in \mathrm{V}⟼\bigcup _{j\in J}\left(b\underset{\dot{}}{\times }j\right)\right)$$
3		comptiunov2.z	$$⊢Z=\left(c\in \mathrm{V}⟼\bigcup _{k\in K}\left(c\underset{\dot{}}{\times }k\right)\right)$$
4		comptiunov2.i	$$⊢I\in \mathrm{V}$$
5		comptiunov2.j	$$⊢J\in \mathrm{V}$$
6		comptiunov2.k	$$⊢K=I\cup J$$
7		comptiunov2.1	$$⊢\bigcup _{k\in I}\left(d\underset{\dot{}}{\times }k\right)\subseteq \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
8		comptiunov2.2	$$⊢\bigcup _{k\in J}\left(d\underset{\dot{}}{\times }k\right)\subseteq \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
9		comptiunov2.3	$$⊢\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)\subseteq \bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)$$
10	1	funmpt2	$$⊢\mathrm{Fun}X$$
11	2	funmpt2	$$⊢\mathrm{Fun}Y$$
12		funco	$$⊢\left(\mathrm{Fun}X\wedge \mathrm{Fun}Y\right)\to \mathrm{Fun}\left(X\circ Y\right)$$
13	10 11 12	mp2an	$$⊢\mathrm{Fun}\left(X\circ Y\right)$$
14	3	funmpt2	$$⊢\mathrm{Fun}Z$$
15		ssv	$$⊢\mathrm{ran}Y\subseteq \mathrm{V}$$
16		ovex	$$⊢a\underset{\dot{}}{\times }i\in \mathrm{V}$$
17	4 16	iunex	$$⊢\bigcup _{i\in I}\left(a\underset{\dot{}}{\times }i\right)\in \mathrm{V}$$
18	17 1	dmmpti	$$⊢\mathrm{dom}X=\mathrm{V}$$
19	15 18	sseqtrri	$$⊢\mathrm{ran}Y\subseteq \mathrm{dom}X$$
20		dmcosseq	$$⊢\mathrm{ran}Y\subseteq \mathrm{dom}X\to \mathrm{dom}\left(X\circ Y\right)=\mathrm{dom}Y$$
21	19 20	ax-mp	$$⊢\mathrm{dom}\left(X\circ Y\right)=\mathrm{dom}Y$$
22		ovex	$$⊢b\underset{\dot{}}{\times }j\in \mathrm{V}$$
23	5 22	iunex	$$⊢\bigcup _{j\in J}\left(b\underset{\dot{}}{\times }j\right)\in \mathrm{V}$$
24	23 2	dmmpti	$$⊢\mathrm{dom}Y=\mathrm{V}$$
25	21 24	eqtri	$$⊢\mathrm{dom}\left(X\circ Y\right)=\mathrm{V}$$
26	4 5	unex	$$⊢I\cup J\in \mathrm{V}$$
27	6 26	eqeltri	$$⊢K\in \mathrm{V}$$
28		ovex	$$⊢c\underset{\dot{}}{\times }k\in \mathrm{V}$$
29	27 28	iunex	$$⊢\bigcup _{k\in K}\left(c\underset{\dot{}}{\times }k\right)\in \mathrm{V}$$
30	29 3	dmmpti	$$⊢\mathrm{dom}Z=\mathrm{V}$$
31	25 30	eqtr4i	$$⊢\mathrm{dom}\left(X\circ Y\right)=\mathrm{dom}Z$$
32		vex	$$⊢d\in \mathrm{V}$$
33	32 24	eleqtrri	$$⊢d\in \mathrm{dom}Y$$
34		fvco	$$⊢\left(\mathrm{Fun}Y\wedge d\in \mathrm{dom}Y\right)\to \left(X\circ Y\right)\left(d\right)=X\left(Y\left(d\right)\right)$$
35	11 33 34	mp2an	$$⊢\left(X\circ Y\right)\left(d\right)=X\left(Y\left(d\right)\right)$$
36		oveq1	$$⊢b=d\to b\underset{\dot{}}{\times }j=d\underset{\dot{}}{\times }j$$
37	36	iuneq2d	$$⊢b=d\to \bigcup _{j\in J}\left(b\underset{\dot{}}{\times }j\right)=\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)$$
38		ovex	$$⊢d\underset{\dot{}}{\times }j\in \mathrm{V}$$
39	5 38	iunex	$$⊢\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\in \mathrm{V}$$
40	37 2 39	fvmpt	$$⊢d\in \mathrm{V}\to Y\left(d\right)=\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)$$
41	40	elv	$$⊢Y\left(d\right)=\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)$$
42	41	fveq2i	$$⊢X\left(Y\left(d\right)\right)=X\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\right)$$
43		oveq1	$$⊢a=\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\to a\underset{\dot{}}{\times }i=\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i$$
44	43	iuneq2d	$$⊢a=\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\to \bigcup _{i\in I}\left(a\underset{\dot{}}{\times }i\right)=\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
45		ovex	$$⊢\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\in \mathrm{V}$$
46	4 45	iunex	$$⊢\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)\in \mathrm{V}$$
47	44 1 46	fvmpt	$$⊢\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\in \mathrm{V}\to X\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\right)=\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
48	39 47	ax-mp	$$⊢X\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\right)=\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
49	35 42 48	3eqtri	$$⊢\left(X\circ Y\right)\left(d\right)=\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
50		oveq1	$$⊢c=d\to c\underset{\dot{}}{\times }k=d\underset{\dot{}}{\times }k$$
51	50	iuneq2d	$$⊢c=d\to \bigcup _{k\in K}\left(c\underset{\dot{}}{\times }k\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
52		ovex	$$⊢d\underset{\dot{}}{\times }k\in \mathrm{V}$$
53	27 52	iunex	$$⊢\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)\in \mathrm{V}$$
54	51 3 53	fvmpt	$$⊢d\in \mathrm{V}\to Z\left(d\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
55	54	elv	$$⊢Z\left(d\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
56	49 55	eqeq12i	$$⊢\left(X\circ Y\right)\left(d\right)=Z\left(d\right)\leftrightarrow \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
57	25 56	raleqbii	$$⊢\forall d\in \mathrm{dom}\left(X\circ Y\right)\left(X\circ Y\right)\left(d\right)=Z\left(d\right)\leftrightarrow \forall d\in \mathrm{V}\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
58		iunxun	$$⊢\bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)=\bigcup _{k\in I}\left(d\underset{\dot{}}{\times }k\right)\cup \bigcup _{k\in J}\left(d\underset{\dot{}}{\times }k\right)$$
59	7 8	unssi	$$⊢\bigcup _{k\in I}\left(d\underset{\dot{}}{\times }k\right)\cup \bigcup _{k\in J}\left(d\underset{\dot{}}{\times }k\right)\subseteq \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
60	58 59	eqsstri	$$⊢\bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)\subseteq \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)$$
61	9 60	eqssi	$$⊢\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)=\bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)$$
62		iuneq1	$$⊢K=I\cup J\to \bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)=\bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)$$
63	6 62	ax-mp	$$⊢\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)=\bigcup _{k\in I\cup J}\left(d\underset{\dot{}}{\times }k\right)$$
64	61 63	eqtr4i	$$⊢\bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
65	64	a1i	$$⊢d\in \mathrm{V}\to \bigcup _{i\in I}\left(\bigcup _{j\in J}\left(d\underset{\dot{}}{\times }j\right)\underset{\dot{}}{\times }i\right)=\bigcup _{k\in K}\left(d\underset{\dot{}}{\times }k\right)$$
66	57 65	mprgbir	$$⊢\forall d\in \mathrm{dom}\left(X\circ Y\right)\left(X\circ Y\right)\left(d\right)=Z\left(d\right)$$
67		eqfunfv	$$⊢\left(\mathrm{Fun}\left(X\circ Y\right)\wedge \mathrm{Fun}Z\right)\to \left(X\circ Y=Z\leftrightarrow \left(\mathrm{dom}\left(X\circ Y\right)=\mathrm{dom}Z\wedge \forall d\in \mathrm{dom}\left(X\circ Y\right)\left(X\circ Y\right)\left(d\right)=Z\left(d\right)\right)\right)$$
68	67	biimprd	$$⊢\left(\mathrm{Fun}\left(X\circ Y\right)\wedge \mathrm{Fun}Z\right)\to \left(\left(\mathrm{dom}\left(X\circ Y\right)=\mathrm{dom}Z\wedge \forall d\in \mathrm{dom}\left(X\circ Y\right)\left(X\circ Y\right)\left(d\right)=Z\left(d\right)\right)\to X\circ Y=Z\right)$$
69	31 66 68	mp2ani	$$⊢\left(\mathrm{Fun}\left(X\circ Y\right)\wedge \mathrm{Fun}Z\right)\to X\circ Y=Z$$
70	13 14 69	mp2an	$$⊢X\circ Y=Z$$