Theorem xpassen 3344

Description: Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254.

Hypotheses

Ref	Expression
xpassen.1	⊢ A ∈ V
xpassen.2	⊢ B ∈ V
xpassen.3	⊢ C ∈ V

Assertion

Ref	Expression
xpassen	⊢ ((A × B) × C) ≈ (A × (B × C))

Proof of Theorem xpassen

Step	Hyp	Ref	Expression
1		xpassen.1	. . . 4 ⊢ A ∈ V
2		xpassen.2	. . . 4 ⊢ B ∈ V
3	1, 2	xpex 2488	. . 3 ⊢ (A × B) ∈ V
4		xpassen.3	. . 3 ⊢ C ∈ V
5	3, 4	xpex 2488	. 2 ⊢ ((A × B) × C) ∈ V
6		opex 1893	. . 3 ⊢ ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩ ∈ V
7	6	a1i 7	. 2 ⊢ (x ∈ ((A × B) × C) → ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩ ∈ V)
8		opex 1893	. . 3 ⊢ ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩ ∈ V
9	8	a1i 7	. 2 ⊢ (y ∈ (A × (B × C)) → ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩ ∈ V)
10		opeq12 1878	. . . . . . . . . . 11 ⊢ ((z = ∪dom {∪dom {x}} ∧ ⟨w, v⟩ = ⟨∪ran {∪dom {x}}, ∪ran {x}⟩) → ⟨z, ⟨w, v⟩⟩ = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩)
11		sneq 1816	. . . . . . . . . . . . . . . . 17 ⊢ (x = ⟨⟨z, w⟩, v⟩ → {x} = {⟨⟨z, w⟩, v⟩})
12	11	dmeqd 2533	. . . . . . . . . . . . . . . 16 ⊢ (x = ⟨⟨z, w⟩, v⟩ → dom {x} = dom {⟨⟨z, w⟩, v⟩})
13	12	unieqd 1929	. . . . . . . . . . . . . . 15 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪dom {x} = ∪dom {⟨⟨z, w⟩, v⟩})
14	13	sneqd 1818	. . . . . . . . . . . . . 14 ⊢ (x = ⟨⟨z, w⟩, v⟩ → {∪dom {x}} = {∪dom {⟨⟨z, w⟩, v⟩}})
15	14	dmeqd 2533	. . . . . . . . . . . . 13 ⊢ (x = ⟨⟨z, w⟩, v⟩ → dom {∪dom {x}} = dom {∪dom {⟨⟨z, w⟩, v⟩}})
16	15	unieqd 1929	. . . . . . . . . . . 12 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪dom {∪dom {x}} = ∪dom {∪dom {⟨⟨z, w⟩, v⟩}})
17		opex 1893	. . . . . . . . . . . . . . . . 17 ⊢ ⟨z, w⟩ ∈ V
18	17	op1sta 2635	. . . . . . . . . . . . . . . 16 ⊢ ∪dom {⟨⟨z, w⟩, v⟩} = ⟨z, w⟩
19	18	sneqi 1817	. . . . . . . . . . . . . . 15 ⊢ {∪dom {⟨⟨z, w⟩, v⟩}} = {⟨z, w⟩}
20	19	dmeqi 2532	. . . . . . . . . . . . . 14 ⊢ dom {∪dom {⟨⟨z, w⟩, v⟩}} = dom {⟨z, w⟩}
21	20	unieqi 1928	. . . . . . . . . . . . 13 ⊢ ∪dom {∪dom {⟨⟨z, w⟩, v⟩}} = ∪dom {⟨z, w⟩}
22		visset 1350	. . . . . . . . . . . . . 14 ⊢ z ∈ V
23	22	op1sta 2635	. . . . . . . . . . . . 13 ⊢ ∪dom {⟨z, w⟩} = z
24	21, 23	eqtr 1119	. . . . . . . . . . . 12 ⊢ ∪dom {∪dom {⟨⟨z, w⟩, v⟩}} = z
25	16, 24	syl6req 1141	. . . . . . . . . . 11 ⊢ (x = ⟨⟨z, w⟩, v⟩ → z = ∪dom {∪dom {x}})
26		opeq12 1878	. . . . . . . . . . . 12 ⊢ ((w = ∪ran {∪dom {x}} ∧ v = ∪ran {x}) → ⟨w, v⟩ = ⟨∪ran {∪dom {x}}, ∪ran {x}⟩)
27	14	rneqd 2557	. . . . . . . . . . . . . 14 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ran {∪dom {x}} = ran {∪dom {⟨⟨z, w⟩, v⟩}})
28	27	unieqd 1929	. . . . . . . . . . . . 13 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪ran {∪dom {x}} = ∪ran {∪dom {⟨⟨z, w⟩, v⟩}})
29	19	rneqi 2556	. . . . . . . . . . . . . . 15 ⊢ ran {∪dom {⟨⟨z, w⟩, v⟩}} = ran {⟨z, w⟩}
30	29	unieqi 1928	. . . . . . . . . . . . . 14 ⊢ ∪ran {∪dom {⟨⟨z, w⟩, v⟩}} = ∪ran {⟨z, w⟩}
31		visset 1350	. . . . . . . . . . . . . . 15 ⊢ w ∈ V
32	22, 31	op2nda 2639	. . . . . . . . . . . . . 14 ⊢ ∪ran {⟨z, w⟩} = w
33	30, 32	eqtr 1119	. . . . . . . . . . . . 13 ⊢ ∪ran {∪dom {⟨⟨z, w⟩, v⟩}} = w
34	28, 33	syl6req 1141	. . . . . . . . . . . 12 ⊢ (x = ⟨⟨z, w⟩, v⟩ → w = ∪ran {∪dom {x}})
35	11	rneqd 2557	. . . . . . . . . . . . . 14 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ran {x} = ran {⟨⟨z, w⟩, v⟩})
36	35	unieqd 1929	. . . . . . . . . . . . 13 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ∪ran {x} = ∪ran {⟨⟨z, w⟩, v⟩})
37		visset 1350	. . . . . . . . . . . . . 14 ⊢ v ∈ V
38	17, 37	op2nda 2639	. . . . . . . . . . . . 13 ⊢ ∪ran {⟨⟨z, w⟩, v⟩} = v
39	36, 38	syl6req 1141	. . . . . . . . . . . 12 ⊢ (x = ⟨⟨z, w⟩, v⟩ → v = ∪ran {x})
40	26, 34, 39	sylanc 361	. . . . . . . . . . 11 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ⟨w, v⟩ = ⟨∪ran {∪dom {x}}, ∪ran {x}⟩)
41	10, 25, 40	sylanc 361	. . . . . . . . . 10 ⊢ (x = ⟨⟨z, w⟩, v⟩ → ⟨z, ⟨w, v⟩⟩ = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩)
42		opeq12 1878	. . . . . . . . . . 11 ⊢ ((⟨z, w⟩ = ⟨∪dom {y}, ∪dom {∪ran {y}}⟩ ∧ v = ∪ran {∪ran {y}}) → ⟨⟨z, w⟩, v⟩ = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩)
43		opeq12 1878	. . . . . . . . . . . 12 ⊢ ((z = ∪dom {y} ∧ w = ∪dom {∪ran {y}}) → ⟨z, w⟩ = ⟨∪dom {y}, ∪dom {∪ran {y}}⟩)
44		sneq 1816	. . . . . . . . . . . . . . 15 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → {y} = {⟨z, ⟨w, v⟩⟩})
45	44	dmeqd 2533	. . . . . . . . . . . . . 14 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → dom {y} = dom {⟨z, ⟨w, v⟩⟩})
46	45	unieqd 1929	. . . . . . . . . . . . 13 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪dom {y} = ∪dom {⟨z, ⟨w, v⟩⟩})
47	22	op1sta 2635	. . . . . . . . . . . . 13 ⊢ ∪dom {⟨z, ⟨w, v⟩⟩} = z
48	46, 47	syl6req 1141	. . . . . . . . . . . 12 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → z = ∪dom {y})
49	44	rneqd 2557	. . . . . . . . . . . . . . . . 17 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ran {y} = ran {⟨z, ⟨w, v⟩⟩})
50	49	unieqd 1929	. . . . . . . . . . . . . . . 16 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪ran {y} = ∪ran {⟨z, ⟨w, v⟩⟩})
51	50	sneqd 1818	. . . . . . . . . . . . . . 15 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → {∪ran {y}} = {∪ran {⟨z, ⟨w, v⟩⟩}})
52	51	dmeqd 2533	. . . . . . . . . . . . . 14 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → dom {∪ran {y}} = dom {∪ran {⟨z, ⟨w, v⟩⟩}})
53	52	unieqd 1929	. . . . . . . . . . . . 13 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪dom {∪ran {y}} = ∪dom {∪ran {⟨z, ⟨w, v⟩⟩}})
54		opex 1893	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨w, v⟩ ∈ V
55	22, 54	op2nda 2639	. . . . . . . . . . . . . . . . 17 ⊢ ∪ran {⟨z, ⟨w, v⟩⟩} = ⟨w, v⟩
56	55	sneqi 1817	. . . . . . . . . . . . . . . 16 ⊢ {∪ran {⟨z, ⟨w, v⟩⟩}} = {⟨w, v⟩}
57	56	dmeqi 2532	. . . . . . . . . . . . . . 15 ⊢ dom {∪ran {⟨z, ⟨w, v⟩⟩}} = dom {⟨w, v⟩}
58	57	unieqi 1928	. . . . . . . . . . . . . 14 ⊢ ∪dom {∪ran {⟨z, ⟨w, v⟩⟩}} = ∪dom {⟨w, v⟩}
59	31	op1sta 2635	. . . . . . . . . . . . . 14 ⊢ ∪dom {⟨w, v⟩} = w
60	58, 59	eqtr 1119	. . . . . . . . . . . . 13 ⊢ ∪dom {∪ran {⟨z, ⟨w, v⟩⟩}} = w
61	53, 60	syl6req 1141	. . . . . . . . . . . 12 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → w = ∪dom {∪ran {y}})
62	43, 48, 61	sylanc 361	. . . . . . . . . . 11 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ⟨z, w⟩ = ⟨∪dom {y}, ∪dom {∪ran {y}}⟩)
63	51	rneqd 2557	. . . . . . . . . . . . 13 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ran {∪ran {y}} = ran {∪ran {⟨z, ⟨w, v⟩⟩}})
64	63	unieqd 1929	. . . . . . . . . . . 12 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ∪ran {∪ran {y}} = ∪ran {∪ran {⟨z, ⟨w, v⟩⟩}})
65	56	rneqi 2556	. . . . . . . . . . . . . 14 ⊢ ran {∪ran {⟨z, ⟨w, v⟩⟩}} = ran {⟨w, v⟩}
66	65	unieqi 1928	. . . . . . . . . . . . 13 ⊢ ∪ran {∪ran {⟨z, ⟨w, v⟩⟩}} = ∪ran {⟨w, v⟩}
67	31, 37	op2nda 2639	. . . . . . . . . . . . 13 ⊢ ∪ran {⟨w, v⟩} = v
68	66, 67	eqtr 1119	. . . . . . . . . . . 12 ⊢ ∪ran {∪ran {⟨z, ⟨w, v⟩⟩}} = v
69	64, 68	syl6req 1141	. . . . . . . . . . 11 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → v = ∪ran {∪ran {y}})
70	42, 62, 69	sylanc 361	. . . . . . . . . 10 ⊢ (y = ⟨z, ⟨w, v⟩⟩ → ⟨⟨z, w⟩, v⟩ = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩)
71	41, 70	cleq2tr 1148	. . . . . . . . 9 ⊢ ((x = ⟨⟨z, w⟩, v⟩ ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (y = ⟨z, ⟨w, v⟩⟩ ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
72		anass 336	. . . . . . . . 9 ⊢ (((z ∈ A ∧ w ∈ B) ∧ v ∈ C) ↔ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))
73	71, 72	anbi12i 369	. . . . . . . 8 ⊢ (((x = ⟨⟨z, w⟩, v⟩ ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ↔ ((y = ⟨z, ⟨w, v⟩⟩ ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩) ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
74		an23 371	. . . . . . . 8 ⊢ (((x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ ((x = ⟨⟨z, w⟩, v⟩ ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)))
75		an23 371	. . . . . . . 8 ⊢ (((y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩) ↔ ((y = ⟨z, ⟨w, v⟩⟩ ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩) ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
76	73, 74, 75	3bitr4 158	. . . . . . 7 ⊢ (((x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ ((y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
77	76	biex 733	. . . . . 6 ⊢ (∃v((x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ ∃v((y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
78		19.41v 963	. . . . . 6 ⊢ (∃v((x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩))
79		19.41v 963	. . . . . 6 ⊢ (∃v((y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩) ↔ (∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
80	77, 78, 79	3bitr3 156	. . . . 5 ⊢ ((∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
81	80	bi2ex 734	. . . 4 ⊢ (∃z∃w(∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ ∃z∃w(∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
82		19.41vv 964	. . . 4 ⊢ (∃z∃w(∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩))
83		19.41vv 964	. . . 4 ⊢ (∃z∃w(∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩) ↔ (∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
84	81, 82, 83	3bitr3 156	. . 3 ⊢ ((∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
85		elxp 2442	. . . . 5 ⊢ (x ∈ ((A × B) × C) ↔ ∃u∃v(x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)))
86		excom 728	. . . . 5 ⊢ (∃u∃v(x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)) ↔ ∃v∃u(x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)))
87		elxp 2442	. . . . . . . . 9 ⊢ (u ∈ (A × B) ↔ ∃z∃w(u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)))
88	87	anbi1i 368	. . . . . . . 8 ⊢ ((u ∈ (A × B) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ (∃z∃w(u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)))
89		an12 370	. . . . . . . 8 ⊢ ((x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)) ↔ (u ∈ (A × B) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)))
90		19.41vv 964	. . . . . . . 8 ⊢ (∃z∃w((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ (∃z∃w(u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)))
91	88, 89, 90	3bitr4 158	. . . . . . 7 ⊢ ((x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)) ↔ ∃z∃w((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)))
92	91	bi2ex 734	. . . . . 6 ⊢ (∃v∃u(x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)) ↔ ∃v∃u∃z∃w((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)))
93		exrot4 778	. . . . . 6 ⊢ (∃v∃u∃z∃w((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ ∃z∃w∃v∃u((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)))
94		anass 336	. . . . . . . . 9 ⊢ (((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ (u = ⟨z, w⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ (x = ⟨u, v⟩ ∧ v ∈ C))))
95	94	biex 733	. . . . . . . 8 ⊢ (∃u((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ ∃u(u = ⟨z, w⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ (x = ⟨u, v⟩ ∧ v ∈ C))))
96		opeq1 1876	. . . . . . . . . . . 12 ⊢ (u = ⟨z, w⟩ → ⟨u, v⟩ = ⟨⟨z, w⟩, v⟩)
97	96	cleq2d 1112	. . . . . . . . . . 11 ⊢ (u = ⟨z, w⟩ → (x = ⟨u, v⟩ ↔ x = ⟨⟨z, w⟩, v⟩))
98	97	anbi1d 469	. . . . . . . . . 10 ⊢ (u = ⟨z, w⟩ → ((x = ⟨u, v⟩ ∧ v ∈ C) ↔ (x = ⟨⟨z, w⟩, v⟩ ∧ v ∈ C)))
99	98	anbi2d 468	. . . . . . . . 9 ⊢ (u = ⟨z, w⟩ → (((z ∈ A ∧ w ∈ B) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ ((z ∈ A ∧ w ∈ B) ∧ (x = ⟨⟨z, w⟩, v⟩ ∧ v ∈ C))))
100	17, 99	ceqsexv 1371	. . . . . . . 8 ⊢ (∃u(u = ⟨z, w⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ (x = ⟨u, v⟩ ∧ v ∈ C))) ↔ ((z ∈ A ∧ w ∈ B) ∧ (x = ⟨⟨z, w⟩, v⟩ ∧ v ∈ C)))
101		an12 370	. . . . . . . 8 ⊢ (((z ∈ A ∧ w ∈ B) ∧ (x = ⟨⟨z, w⟩, v⟩ ∧ v ∈ C)) ↔ (x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)))
102	95, 100, 101	3bitr 155	. . . . . . 7 ⊢ (∃u((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ (x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)))
103	102	bi3ex 735	. . . . . 6 ⊢ (∃z∃w∃v∃u((u = ⟨z, w⟩ ∧ (z ∈ A ∧ w ∈ B)) ∧ (x = ⟨u, v⟩ ∧ v ∈ C)) ↔ ∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)))
104	92, 93, 103	3bitr 155	. . . . 5 ⊢ (∃v∃u(x = ⟨u, v⟩ ∧ (u ∈ (A × B) ∧ v ∈ C)) ↔ ∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)))
105	85, 86, 104	3bitr 155	. . . 4 ⊢ (x ∈ ((A × B) × C) ↔ ∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)))
106	105	anbi1i 368	. . 3 ⊢ ((x ∈ ((A × B) × C) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (∃z∃w∃v(x = ⟨⟨z, w⟩, v⟩ ∧ ((z ∈ A ∧ w ∈ B) ∧ v ∈ C)) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩))
107		elxp 2442	. . . . 5 ⊢ (y ∈ (A × (B × C)) ↔ ∃z∃u(y = ⟨z, u⟩ ∧ (z ∈ A ∧ u ∈ (B × C))))
108		elxp 2442	. . . . . . . . . 10 ⊢ (u ∈ (B × C) ↔ ∃w∃v(u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C)))
109	108	anbi2i 367	. . . . . . . . 9 ⊢ (((y = ⟨z, u⟩ ∧ z ∈ A) ∧ u ∈ (B × C)) ↔ ((y = ⟨z, u⟩ ∧ z ∈ A) ∧ ∃w∃v(u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))))
110		anass 336	. . . . . . . . 9 ⊢ (((y = ⟨z, u⟩ ∧ z ∈ A) ∧ u ∈ (B × C)) ↔ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ u ∈ (B × C))))
111		19.42vv 968	. . . . . . . . . 10 ⊢ (∃w∃v((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))) ↔ ((y = ⟨z, u⟩ ∧ z ∈ A) ∧ ∃w∃v(u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))))
112		an12 370	. . . . . . . . . . . 12 ⊢ (((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))) ↔ (u = ⟨w, v⟩ ∧ ((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (w ∈ B ∧ v ∈ C))))
113		anass 336	. . . . . . . . . . . . 13 ⊢ (((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (w ∈ B ∧ v ∈ C)) ↔ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
114	113	anbi2i 367	. . . . . . . . . . . 12 ⊢ ((u = ⟨w, v⟩ ∧ ((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (w ∈ B ∧ v ∈ C))) ↔ (u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
115	112, 114	bitr 151	. . . . . . . . . . 11 ⊢ (((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))) ↔ (u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
116	115	bi2ex 734	. . . . . . . . . 10 ⊢ (∃w∃v((y = ⟨z, u⟩ ∧ z ∈ A) ∧ (u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))) ↔ ∃w∃v(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
117	111, 116	bitr3 153	. . . . . . . . 9 ⊢ (((y = ⟨z, u⟩ ∧ z ∈ A) ∧ ∃w∃v(u = ⟨w, v⟩ ∧ (w ∈ B ∧ v ∈ C))) ↔ ∃w∃v(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
118	109, 110, 117	3bitr3 156	. . . . . . . 8 ⊢ ((y = ⟨z, u⟩ ∧ (z ∈ A ∧ u ∈ (B × C))) ↔ ∃w∃v(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
119	118	biex 733	. . . . . . 7 ⊢ (∃u(y = ⟨z, u⟩ ∧ (z ∈ A ∧ u ∈ (B × C))) ↔ ∃u∃w∃v(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
120		exrot3 777	. . . . . . 7 ⊢ (∃u∃w∃v(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))) ↔ ∃w∃v∃u(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
121		opeq2 1877	. . . . . . . . . . 11 ⊢ (u = ⟨w, v⟩ → ⟨z, u⟩ = ⟨z, ⟨w, v⟩⟩)
122	121	cleq2d 1112	. . . . . . . . . 10 ⊢ (u = ⟨w, v⟩ → (y = ⟨z, u⟩ ↔ y = ⟨z, ⟨w, v⟩⟩))
123	122	anbi1d 469	. . . . . . . . 9 ⊢ (u = ⟨w, v⟩ → ((y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ↔ (y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))))
124	54, 123	ceqsexv 1371	. . . . . . . 8 ⊢ (∃u(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))) ↔ (y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
125	124	bi2ex 734	. . . . . . 7 ⊢ (∃w∃v∃u(u = ⟨w, v⟩ ∧ (y = ⟨z, u⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C)))) ↔ ∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
126	119, 120, 125	3bitr 155	. . . . . 6 ⊢ (∃u(y = ⟨z, u⟩ ∧ (z ∈ A ∧ u ∈ (B × C))) ↔ ∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
127	126	biex 733	. . . . 5 ⊢ (∃z∃u(y = ⟨z, u⟩ ∧ (z ∈ A ∧ u ∈ (B × C))) ↔ ∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
128	107, 127	bitr 151	. . . 4 ⊢ (y ∈ (A × (B × C)) ↔ ∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))))
129	128	anbi1i 368	. . 3 ⊢ ((y ∈ (A × (B × C)) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩) ↔ (∃z∃w∃v(y = ⟨z, ⟨w, v⟩⟩ ∧ (z ∈ A ∧ (w ∈ B ∧ v ∈ C))) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
130	84, 106, 129	3bitr4 158	. 2 ⊢ ((x ∈ ((A × B) × C) ∧ y = ⟨∪dom {∪dom {x}}, ⟨∪ran {∪dom {x}}, ∪ran {x}⟩⟩) ↔ (y ∈ (A × (B × C)) ∧ x = ⟨⟨∪dom {y}, ∪dom {∪ran {y}}⟩, ∪ran {∪ran {y}}⟩))
131	5, 7, 9, 130	en2 3305	1 ⊢ ((A × B) × C) ≈ (A × (B × C))

Syntax hints:   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  Vcvv 1348  {csn 1808  ⟨cop 1810  ∪cuni 1919   class class class wbr 2054   × cxp 2408  dom cdm 2410  ran crn 2411   ≈ cen 3271

This theorem is referenced by:  cdaassen 3725  xpcdaen 3726

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-im