Theorem xpassen

Description: Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of Mendelson p. 254. (Contributed by NM, 22-Jan-2004) (Revised by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Hypotheses	xpassen.1	$$⊢A\in \mathrm{V}$$
	xpassen.2	$$⊢B\in \mathrm{V}$$
	xpassen.3	$$⊢C\in \mathrm{V}$$
Assertion	xpassen	$$⊢\left(\left(A\times B\right)\times C\right)\approx \left(A\times \left(B\times C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpassen.1	$$⊢A\in \mathrm{V}$$
2		xpassen.2	$$⊢B\in \mathrm{V}$$
3		xpassen.3	$$⊢C\in \mathrm{V}$$
4	1 2	xpex	$$⊢A\times B\in \mathrm{V}$$
5	4 3	xpex	$$⊢\left(A\times B\right)\times C\in \mathrm{V}$$
6	2 3	xpex	$$⊢B\times C\in \mathrm{V}$$
7	1 6	xpex	$$⊢A\times \left(B\times C\right)\in \mathrm{V}$$
8		opex	$$⊢⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\in \mathrm{V}$$
9	8	a1i	$$⊢x\in \left(\left(A\times B\right)\times C\right)\to ⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\in \mathrm{V}$$
10		opex	$$⊢⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\in \mathrm{V}$$
11	10	a1i	$$⊢y\in \left(A\times \left(B\times C\right)\right)\to ⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\in \mathrm{V}$$
12		sneq	$$⊢x=⟨⟨z,w⟩,v⟩\to \left\{x\right\}=\left\{⟨⟨z,w⟩,v⟩\right\}$$
13	12	dmeqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \mathrm{dom}\left\{x\right\}=\mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}$$
14	13	unieqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \bigcup \mathrm{dom}\left\{x\right\}=\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}$$
15	14	sneqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}=\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}$$
16	15	dmeqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}=\mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}$$
17	16	unieqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}=\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}$$
18		opex	$$⊢⟨z,w⟩\in \mathrm{V}$$
19		vex	$$⊢v\in \mathrm{V}$$
20	18 19	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}=⟨z,w⟩$$
21	20	sneqi	$$⊢\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=\left\{⟨z,w⟩\right\}$$
22	21	dmeqi	$$⊢\mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=\mathrm{dom}\left\{⟨z,w⟩\right\}$$
23	22	unieqi	$$⊢\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=\bigcup \mathrm{dom}\left\{⟨z,w⟩\right\}$$
24		vex	$$⊢z\in \mathrm{V}$$
25		vex	$$⊢w\in \mathrm{V}$$
26	24 25	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨z,w⟩\right\}=z$$
27	23 26	eqtri	$$⊢\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=z$$
28	17 27	syl6req	$$⊢x=⟨⟨z,w⟩,v⟩\to z=\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}$$
29	15	rneqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}=\mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}$$
30	29	unieqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}=\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}$$
31	21	rneqi	$$⊢\mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=\mathrm{ran}\left\{⟨z,w⟩\right\}$$
32	31	unieqi	$$⊢\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=\bigcup \mathrm{ran}\left\{⟨z,w⟩\right\}$$
33	24 25	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨z,w⟩\right\}=w$$
34	32 33	eqtri	$$⊢\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{⟨⟨z,w⟩,v⟩\right\}\right\}=w$$
35	30 34	syl6req	$$⊢x=⟨⟨z,w⟩,v⟩\to w=\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\}$$
36	12	rneqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \mathrm{ran}\left\{x\right\}=\mathrm{ran}\left\{⟨⟨z,w⟩,v⟩\right\}$$
37	36	unieqd	$$⊢x=⟨⟨z,w⟩,v⟩\to \bigcup \mathrm{ran}\left\{x\right\}=\bigcup \mathrm{ran}\left\{⟨⟨z,w⟩,v⟩\right\}$$
38	18 19	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨⟨z,w⟩,v⟩\right\}=v$$
39	37 38	syl6req	$$⊢x=⟨⟨z,w⟩,v⟩\to v=\bigcup \mathrm{ran}\left\{x\right\}$$
40	35 39	opeq12d	$$⊢x=⟨⟨z,w⟩,v⟩\to ⟨w,v⟩=⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩$$
41	28 40	opeq12d	$$⊢x=⟨⟨z,w⟩,v⟩\to ⟨z,⟨w,v⟩⟩=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩$$
42		sneq	$$⊢y=⟨z,⟨w,v⟩⟩\to \left\{y\right\}=\left\{⟨z,⟨w,v⟩⟩\right\}$$
43	42	dmeqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \mathrm{dom}\left\{y\right\}=\mathrm{dom}\left\{⟨z,⟨w,v⟩⟩\right\}$$
44	43	unieqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \bigcup \mathrm{dom}\left\{y\right\}=\bigcup \mathrm{dom}\left\{⟨z,⟨w,v⟩⟩\right\}$$
45		opex	$$⊢⟨w,v⟩\in \mathrm{V}$$
46	24 45	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨z,⟨w,v⟩⟩\right\}=z$$
47	44 46	syl6req	$$⊢y=⟨z,⟨w,v⟩⟩\to z=\bigcup \mathrm{dom}\left\{y\right\}$$
48	42	rneqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \mathrm{ran}\left\{y\right\}=\mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}$$
49	48	unieqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \bigcup \mathrm{ran}\left\{y\right\}=\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}$$
50	49	sneqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}=\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}$$
51	50	dmeqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}=\mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}$$
52	51	unieqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}=\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}$$
53	24 45	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}=⟨w,v⟩$$
54	53	sneqi	$$⊢\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=\left\{⟨w,v⟩\right\}$$
55	54	dmeqi	$$⊢\mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=\mathrm{dom}\left\{⟨w,v⟩\right\}$$
56	55	unieqi	$$⊢\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=\bigcup \mathrm{dom}\left\{⟨w,v⟩\right\}$$
57	25 19	op1sta	$$⊢\bigcup \mathrm{dom}\left\{⟨w,v⟩\right\}=w$$
58	56 57	eqtri	$$⊢\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=w$$
59	52 58	syl6req	$$⊢y=⟨z,⟨w,v⟩⟩\to w=\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}$$
60	47 59	opeq12d	$$⊢y=⟨z,⟨w,v⟩⟩\to ⟨z,w⟩=⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩$$
61	50	rneqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}=\mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}$$
62	61	unieqd	$$⊢y=⟨z,⟨w,v⟩⟩\to \bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}=\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}$$
63	54	rneqi	$$⊢\mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=\mathrm{ran}\left\{⟨w,v⟩\right\}$$
64	63	unieqi	$$⊢\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=\bigcup \mathrm{ran}\left\{⟨w,v⟩\right\}$$
65	25 19	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨w,v⟩\right\}=v$$
66	64 65	eqtri	$$⊢\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{⟨z,⟨w,v⟩⟩\right\}\right\}=v$$
67	62 66	syl6req	$$⊢y=⟨z,⟨w,v⟩⟩\to v=\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}$$
68	60 67	opeq12d	$$⊢y=⟨z,⟨w,v⟩⟩\to ⟨⟨z,w⟩,v⟩=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩$$
69	41 68	eq2tri	$$⊢\left(x=⟨⟨z,w⟩,v⟩\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(y=⟨z,⟨w,v⟩⟩\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
70		anass	$$⊢\left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\leftrightarrow \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)$$
71	69 70	anbi12i	$$⊢\left(\left(x=⟨⟨z,w⟩,v⟩\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\leftrightarrow \left(\left(y=⟨z,⟨w,v⟩⟩\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
72		an32	$$⊢\left(\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\left(x=⟨⟨z,w⟩,v⟩\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)$$
73		an32	$$⊢\left(\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)\leftrightarrow \left(\left(y=⟨z,⟨w,v⟩⟩\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
74	71 72 73	3bitr4i	$$⊢\left(\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
75	74	exbii	$$⊢\exists v\left(\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \exists v\left(\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
76		19.41v	$$⊢\exists v\left(\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)$$
77		19.41v	$$⊢\exists v\left(\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)\leftrightarrow \left(\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
78	75 76 77	3bitr3i	$$⊢\left(\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
79	78	2exbii	$$⊢\exists z\exists w\left(\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \exists z\exists w\left(\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
80		19.41vv	$$⊢\exists z\exists w\left(\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\exists z\exists w\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)$$
81		19.41vv	$$⊢\exists z\exists w\left(\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)\leftrightarrow \left(\exists z\exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
82	79 80 81	3bitr3i	$$⊢\left(\exists z\exists w\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\exists z\exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
83		elxp	$$⊢x\in \left(\left(A\times B\right)\times C\right)\leftrightarrow \exists u\exists v\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)$$
84		excom	$$⊢\exists u\exists v\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)\leftrightarrow \exists v\exists u\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)$$
85		elxp	$$⊢u\in \left(A\times B\right)\leftrightarrow \exists z\exists w\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)$$
86	85	anbi1i	$$⊢\left(u\in \left(A\times B\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \left(\exists z\exists w\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)$$
87		an12	$$⊢\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)\leftrightarrow \left(u\in \left(A\times B\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)$$
88		19.41vv	$$⊢\exists z\exists w\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \left(\exists z\exists w\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)$$
89	86 87 88	3bitr4i	$$⊢\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)\leftrightarrow \exists z\exists w\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)$$
90	89	2exbii	$$⊢\exists v\exists u\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)\leftrightarrow \exists v\exists u\exists z\exists w\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)$$
91		exrot4	$$⊢\exists v\exists u\exists z\exists w\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \exists z\exists w\exists v\exists u\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)$$
92		anass	$$⊢\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \left(u=⟨z,w⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\right)$$
93	92	exbii	$$⊢\exists u\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \exists u\left(u=⟨z,w⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\right)$$
94		opeq1	$$⊢u=⟨z,w⟩\to ⟨u,v⟩=⟨⟨z,w⟩,v⟩$$
95	94	eqeq2d	$$⊢u=⟨z,w⟩\to \left(x=⟨u,v⟩\leftrightarrow x=⟨⟨z,w⟩,v⟩\right)$$
96	95	anbi1d	$$⊢u=⟨z,w⟩\to \left(\left(x=⟨u,v⟩\wedge v\in C\right)\leftrightarrow \left(x=⟨⟨z,w⟩,v⟩\wedge v\in C\right)\right)$$
97	96	anbi2d	$$⊢u=⟨z,w⟩\to \left(\left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨⟨z,w⟩,v⟩\wedge v\in C\right)\right)\right)$$
98	18 97	ceqsexv	$$⊢\exists u\left(u=⟨z,w⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\right)\leftrightarrow \left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨⟨z,w⟩,v⟩\wedge v\in C\right)\right)$$
99		an12	$$⊢\left(\left(z\in A\wedge w\in B\right)\wedge \left(x=⟨⟨z,w⟩,v⟩\wedge v\in C\right)\right)\leftrightarrow \left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)$$
100	93 98 99	3bitri	$$⊢\exists u\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)$$
101	100	3exbii	$$⊢\exists z\exists w\exists v\exists u\left(\left(u=⟨z,w⟩\wedge \left(z\in A\wedge w\in B\right)\right)\wedge \left(x=⟨u,v⟩\wedge v\in C\right)\right)\leftrightarrow \exists z\exists w\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)$$
102	90 91 101	3bitri	$$⊢\exists v\exists u\left(x=⟨u,v⟩\wedge \left(u\in \left(A\times B\right)\wedge v\in C\right)\right)\leftrightarrow \exists z\exists w\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)$$
103	83 84 102	3bitri	$$⊢x\in \left(\left(A\times B\right)\times C\right)\leftrightarrow \exists z\exists w\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)$$
104	103	anbi1i	$$⊢\left(x\in \left(\left(A\times B\right)\times C\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(\exists z\exists w\exists v\left(x=⟨⟨z,w⟩,v⟩\wedge \left(\left(z\in A\wedge w\in B\right)\wedge v\in C\right)\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)$$
105		elxp	$$⊢y\in \left(A\times \left(B\times C\right)\right)\leftrightarrow \exists z\exists u\left(y=⟨z,u⟩\wedge \left(z\in A\wedge u\in \left(B\times C\right)\right)\right)$$
106		elxp	$$⊢u\in \left(B\times C\right)\leftrightarrow \exists w\exists v\left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)$$
107	106	anbi2i	$$⊢\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge u\in \left(B\times C\right)\right)\leftrightarrow \left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \exists w\exists v\left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
108		anass	$$⊢\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge u\in \left(B\times C\right)\right)\leftrightarrow \left(y=⟨z,u⟩\wedge \left(z\in A\wedge u\in \left(B\times C\right)\right)\right)$$
109		19.42vv	$$⊢\exists w\exists v\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \exists w\exists v\left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
110		an12	$$⊢\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \left(u=⟨w,v⟩\wedge \left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
111		anass	$$⊢\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(w\in B\wedge v\in C\right)\right)\leftrightarrow \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
112	111	anbi2i	$$⊢\left(u=⟨w,v⟩\wedge \left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
113	110 112	bitri	$$⊢\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
114	113	2exbii	$$⊢\exists w\exists v\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \exists w\exists v\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
115	109 114	bitr3i	$$⊢\left(\left(y=⟨z,u⟩\wedge z\in A\right)\wedge \exists w\exists v\left(u=⟨w,v⟩\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \exists w\exists v\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
116	107 108 115	3bitr3i	$$⊢\left(y=⟨z,u⟩\wedge \left(z\in A\wedge u\in \left(B\times C\right)\right)\right)\leftrightarrow \exists w\exists v\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
117	116	exbii	$$⊢\exists u\left(y=⟨z,u⟩\wedge \left(z\in A\wedge u\in \left(B\times C\right)\right)\right)\leftrightarrow \exists u\exists w\exists v\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
118		exrot3	$$⊢\exists u\exists w\exists v\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)\leftrightarrow \exists w\exists v\exists u\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
119		opeq2	$$⊢u=⟨w,v⟩\to ⟨z,u⟩=⟨z,⟨w,v⟩⟩$$
120	119	eqeq2d	$$⊢u=⟨w,v⟩\to \left(y=⟨z,u⟩\leftrightarrow y=⟨z,⟨w,v⟩⟩\right)$$
121	120	anbi1d	$$⊢u=⟨w,v⟩\to \left(\left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\leftrightarrow \left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)$$
122	45 121	ceqsexv	$$⊢\exists u\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)\leftrightarrow \left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
123	122	2exbii	$$⊢\exists w\exists v\exists u\left(u=⟨w,v⟩\wedge \left(y=⟨z,u⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\right)\leftrightarrow \exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
124	117 118 123	3bitri	$$⊢\exists u\left(y=⟨z,u⟩\wedge \left(z\in A\wedge u\in \left(B\times C\right)\right)\right)\leftrightarrow \exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
125	124	exbii	$$⊢\exists z\exists u\left(y=⟨z,u⟩\wedge \left(z\in A\wedge u\in \left(B\times C\right)\right)\right)\leftrightarrow \exists z\exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
126	105 125	bitri	$$⊢y\in \left(A\times \left(B\times C\right)\right)\leftrightarrow \exists z\exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)$$
127	126	anbi1i	$$⊢\left(y\in \left(A\times \left(B\times C\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)\leftrightarrow \left(\exists z\exists w\exists v\left(y=⟨z,⟨w,v⟩⟩\wedge \left(z\in A\wedge \left(w\in B\wedge v\in C\right)\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
128	82 104 127	3bitr4i	$$⊢\left(x\in \left(\left(A\times B\right)\times C\right)\wedge y=⟨\bigcup \mathrm{dom}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},⟨\bigcup \mathrm{ran}\left\{\bigcup \mathrm{dom}\left\{x\right\}\right\},\bigcup \mathrm{ran}\left\{x\right\}⟩⟩\right)\leftrightarrow \left(y\in \left(A\times \left(B\times C\right)\right)\wedge x=⟨⟨\bigcup \mathrm{dom}\left\{y\right\},\bigcup \mathrm{dom}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩,\bigcup \mathrm{ran}\left\{\bigcup \mathrm{ran}\left\{y\right\}\right\}⟩\right)$$
129	5 7 9 11 128	en2i	$$⊢\left(\left(A\times B\right)\times C\right)\approx \left(A\times \left(B\times C\right)\right)$$