ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpassen Structured version   GIF version

Theorem xpassen 6240
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.)
Hypotheses
Ref Expression
xpassen.1 A V
xpassen.2 B V
xpassen.3 𝐶 V
Assertion
Ref Expression
xpassen ((A × B) × 𝐶) ≈ (A × (B × 𝐶))

Proof of Theorem xpassen
Dummy variables x y z w v u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpassen.1 . . . 4 A V
2 xpassen.2 . . . 4 B V
31, 2xpex 4396 . . 3 (A × B) V
4 xpassen.3 . . 3 𝐶 V
53, 4xpex 4396 . 2 ((A × B) × 𝐶) V
62, 4xpex 4396 . . 3 (B × 𝐶) V
71, 6xpex 4396 . 2 (A × (B × 𝐶)) V
8 vex 2554 . . . . . . . . . 10 x V
98snex 3928 . . . . . . . . 9 {x} V
109dmex 4541 . . . . . . . 8 dom {x} V
1110uniex 4140 . . . . . . 7 dom {x} V
1211snex 3928 . . . . . 6 { dom {x}} V
1312dmex 4541 . . . . 5 dom { dom {x}} V
1413uniex 4140 . . . 4 dom { dom {x}} V
1512rnex 4542 . . . . . 6 ran { dom {x}} V
1615uniex 4140 . . . . 5 ran { dom {x}} V
179rnex 4542 . . . . . 6 ran {x} V
1817uniex 4140 . . . . 5 ran {x} V
1916, 18opex 3957 . . . 4 ran { dom {x}}, ran {x}⟩ V
2014, 19opex 3957 . . 3 dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩ V
2120a1i 9 . 2 (x ((A × B) × 𝐶) → ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩ V)
22 vex 2554 . . . . . . . 8 y V
2322snex 3928 . . . . . . 7 {y} V
2423dmex 4541 . . . . . 6 dom {y} V
2524uniex 4140 . . . . 5 dom {y} V
2623rnex 4542 . . . . . . . . 9 ran {y} V
2726uniex 4140 . . . . . . . 8 ran {y} V
2827snex 3928 . . . . . . 7 { ran {y}} V
2928dmex 4541 . . . . . 6 dom { ran {y}} V
3029uniex 4140 . . . . 5 dom { ran {y}} V
3125, 30opex 3957 . . . 4 dom {y}, dom { ran {y}}⟩ V
3228rnex 4542 . . . . 5 ran { ran {y}} V
3332uniex 4140 . . . 4 ran { ran {y}} V
3431, 33opex 3957 . . 3 ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩ V
3534a1i 9 . 2 (y (A × (B × 𝐶)) → ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩ V)
36 sneq 3378 . . . . . . . . . . . . . . . . 17 (x = ⟨⟨z, w⟩, v⟩ → {x} = {⟨⟨z, w⟩, v⟩})
3736dmeqd 4480 . . . . . . . . . . . . . . . 16 (x = ⟨⟨z, w⟩, v⟩ → dom {x} = dom {⟨⟨z, w⟩, v⟩})
3837unieqd 3582 . . . . . . . . . . . . . . 15 (x = ⟨⟨z, w⟩, v⟩ → dom {x} = dom {⟨⟨z, w⟩, v⟩})
3938sneqd 3380 . . . . . . . . . . . . . 14 (x = ⟨⟨z, w⟩, v⟩ → { dom {x}} = { dom {⟨⟨z, w⟩, v⟩}})
4039dmeqd 4480 . . . . . . . . . . . . 13 (x = ⟨⟨z, w⟩, v⟩ → dom { dom {x}} = dom { dom {⟨⟨z, w⟩, v⟩}})
4140unieqd 3582 . . . . . . . . . . . 12 (x = ⟨⟨z, w⟩, v⟩ → dom { dom {x}} = dom { dom {⟨⟨z, w⟩, v⟩}})
42 vex 2554 . . . . . . . . . . . . . . . . . 18 z V
43 vex 2554 . . . . . . . . . . . . . . . . . 18 w V
4442, 43opex 3957 . . . . . . . . . . . . . . . . 17 z, w V
45 vex 2554 . . . . . . . . . . . . . . . . 17 v V
4644, 45op1sta 4745 . . . . . . . . . . . . . . . 16 dom {⟨⟨z, w⟩, v⟩} = ⟨z, w
4746sneqi 3379 . . . . . . . . . . . . . . 15 { dom {⟨⟨z, w⟩, v⟩}} = {⟨z, w⟩}
4847dmeqi 4479 . . . . . . . . . . . . . 14 dom { dom {⟨⟨z, w⟩, v⟩}} = dom {⟨z, w⟩}
4948unieqi 3581 . . . . . . . . . . . . 13 dom { dom {⟨⟨z, w⟩, v⟩}} = dom {⟨z, w⟩}
5042, 43op1sta 4745 . . . . . . . . . . . . 13 dom {⟨z, w⟩} = z
5149, 50eqtri 2057 . . . . . . . . . . . 12 dom { dom {⟨⟨z, w⟩, v⟩}} = z
5241, 51syl6req 2086 . . . . . . . . . . 11 (x = ⟨⟨z, w⟩, v⟩ → z = dom { dom {x}})
5339rneqd 4506 . . . . . . . . . . . . . 14 (x = ⟨⟨z, w⟩, v⟩ → ran { dom {x}} = ran { dom {⟨⟨z, w⟩, v⟩}})
5453unieqd 3582 . . . . . . . . . . . . 13 (x = ⟨⟨z, w⟩, v⟩ → ran { dom {x}} = ran { dom {⟨⟨z, w⟩, v⟩}})
5547rneqi 4505 . . . . . . . . . . . . . . 15 ran { dom {⟨⟨z, w⟩, v⟩}} = ran {⟨z, w⟩}
5655unieqi 3581 . . . . . . . . . . . . . 14 ran { dom {⟨⟨z, w⟩, v⟩}} = ran {⟨z, w⟩}
5742, 43op2nda 4748 . . . . . . . . . . . . . 14 ran {⟨z, w⟩} = w
5856, 57eqtri 2057 . . . . . . . . . . . . 13 ran { dom {⟨⟨z, w⟩, v⟩}} = w
5954, 58syl6req 2086 . . . . . . . . . . . 12 (x = ⟨⟨z, w⟩, v⟩ → w = ran { dom {x}})
6036rneqd 4506 . . . . . . . . . . . . . 14 (x = ⟨⟨z, w⟩, v⟩ → ran {x} = ran {⟨⟨z, w⟩, v⟩})
6160unieqd 3582 . . . . . . . . . . . . 13 (x = ⟨⟨z, w⟩, v⟩ → ran {x} = ran {⟨⟨z, w⟩, v⟩})
6244, 45op2nda 4748 . . . . . . . . . . . . 13 ran {⟨⟨z, w⟩, v⟩} = v
6361, 62syl6req 2086 . . . . . . . . . . . 12 (x = ⟨⟨z, w⟩, v⟩ → v = ran {x})
6459, 63opeq12d 3548 . . . . . . . . . . 11 (x = ⟨⟨z, w⟩, v⟩ → ⟨w, v⟩ = ⟨ ran { dom {x}}, ran {x}⟩)
6552, 64opeq12d 3548 . . . . . . . . . 10 (x = ⟨⟨z, w⟩, v⟩ → ⟨z, ⟨w, v⟩⟩ = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩)
66 sneq 3378 . . . . . . . . . . . . . . 15 (y = ⟨z, ⟨w, v⟩⟩ → {y} = {⟨z, ⟨w, v⟩⟩})
6766dmeqd 4480 . . . . . . . . . . . . . 14 (y = ⟨z, ⟨w, v⟩⟩ → dom {y} = dom {⟨z, ⟨w, v⟩⟩})
6867unieqd 3582 . . . . . . . . . . . . 13 (y = ⟨z, ⟨w, v⟩⟩ → dom {y} = dom {⟨z, ⟨w, v⟩⟩})
6943, 45opex 3957 . . . . . . . . . . . . . 14 w, v V
7042, 69op1sta 4745 . . . . . . . . . . . . 13 dom {⟨z, ⟨w, v⟩⟩} = z
7168, 70syl6req 2086 . . . . . . . . . . . 12 (y = ⟨z, ⟨w, v⟩⟩ → z = dom {y})
7266rneqd 4506 . . . . . . . . . . . . . . . . 17 (y = ⟨z, ⟨w, v⟩⟩ → ran {y} = ran {⟨z, ⟨w, v⟩⟩})
7372unieqd 3582 . . . . . . . . . . . . . . . 16 (y = ⟨z, ⟨w, v⟩⟩ → ran {y} = ran {⟨z, ⟨w, v⟩⟩})
7473sneqd 3380 . . . . . . . . . . . . . . 15 (y = ⟨z, ⟨w, v⟩⟩ → { ran {y}} = { ran {⟨z, ⟨w, v⟩⟩}})
7574dmeqd 4480 . . . . . . . . . . . . . 14 (y = ⟨z, ⟨w, v⟩⟩ → dom { ran {y}} = dom { ran {⟨z, ⟨w, v⟩⟩}})
7675unieqd 3582 . . . . . . . . . . . . 13 (y = ⟨z, ⟨w, v⟩⟩ → dom { ran {y}} = dom { ran {⟨z, ⟨w, v⟩⟩}})
7742, 69op2nda 4748 . . . . . . . . . . . . . . . . 17 ran {⟨z, ⟨w, v⟩⟩} = ⟨w, v
7877sneqi 3379 . . . . . . . . . . . . . . . 16 { ran {⟨z, ⟨w, v⟩⟩}} = {⟨w, v⟩}
7978dmeqi 4479 . . . . . . . . . . . . . . 15 dom { ran {⟨z, ⟨w, v⟩⟩}} = dom {⟨w, v⟩}
8079unieqi 3581 . . . . . . . . . . . . . 14 dom { ran {⟨z, ⟨w, v⟩⟩}} = dom {⟨w, v⟩}
8143, 45op1sta 4745 . . . . . . . . . . . . . 14 dom {⟨w, v⟩} = w
8280, 81eqtri 2057 . . . . . . . . . . . . 13 dom { ran {⟨z, ⟨w, v⟩⟩}} = w
8376, 82syl6req 2086 . . . . . . . . . . . 12 (y = ⟨z, ⟨w, v⟩⟩ → w = dom { ran {y}})
8471, 83opeq12d 3548 . . . . . . . . . . 11 (y = ⟨z, ⟨w, v⟩⟩ → ⟨z, w⟩ = ⟨ dom {y}, dom { ran {y}}⟩)
8574rneqd 4506 . . . . . . . . . . . . 13 (y = ⟨z, ⟨w, v⟩⟩ → ran { ran {y}} = ran { ran {⟨z, ⟨w, v⟩⟩}})
8685unieqd 3582 . . . . . . . . . . . 12 (y = ⟨z, ⟨w, v⟩⟩ → ran { ran {y}} = ran { ran {⟨z, ⟨w, v⟩⟩}})
8778rneqi 4505 . . . . . . . . . . . . . 14 ran { ran {⟨z, ⟨w, v⟩⟩}} = ran {⟨w, v⟩}
8887unieqi 3581 . . . . . . . . . . . . 13 ran { ran {⟨z, ⟨w, v⟩⟩}} = ran {⟨w, v⟩}
8943, 45op2nda 4748 . . . . . . . . . . . . 13 ran {⟨w, v⟩} = v
9088, 89eqtri 2057 . . . . . . . . . . . 12 ran { ran {⟨z, ⟨w, v⟩⟩}} = v
9186, 90syl6req 2086 . . . . . . . . . . 11 (y = ⟨z, ⟨w, v⟩⟩ → v = ran { ran {y}})
9284, 91opeq12d 3548 . . . . . . . . . 10 (y = ⟨z, ⟨w, v⟩⟩ → ⟨⟨z, w⟩, v⟩ = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩)
9365, 92eq2tri 2096 . . . . . . . . 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}}⟩))
94 anass 381 . . . . . . . . 9 (((z A w B) v 𝐶) ↔ (z A (w B v 𝐶)))
9593, 94anbi12i 433 . . . . . . . 8 (((x = ⟨⟨z, w⟩, v y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ((z A w B) v 𝐶)) ↔ ((y = ⟨z, ⟨w, v⟩⟩ x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩) (z A (w B v 𝐶))))
96 an32 496 . . . . . . . 8 (((x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) 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 𝐶)))
97 an32 496 . . . . . . . 8 (((y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) 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 𝐶))))
9895, 96, 973bitr4i 201 . . . . . . 7 (((x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ ((y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
9998exbii 1493 . . . . . 6 (v((x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ v((y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
100 19.41v 1779 . . . . . 6 (v((x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ (v(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩))
101 19.41v 1779 . . . . . 6 (v((y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩) ↔ (v(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
10299, 100, 1013bitr3i 199 . . . . 5 ((v(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ (v(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
1031022exbii 1494 . . . 4 (zw(v(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ zw(v(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
104 19.41vv 1780 . . . 4 (zw(v(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ (zwv(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩))
105 19.41vv 1780 . . . 4 (zw(v(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩) ↔ (zwv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
106103, 104, 1053bitr3i 199 . . 3 ((zwv(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ (zwv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
107 elxp 4305 . . . . 5 (x ((A × B) × 𝐶) ↔ uv(x = ⟨u, v (u (A × B) v 𝐶)))
108 excom 1551 . . . . 5 (uv(x = ⟨u, v (u (A × B) v 𝐶)) ↔ vu(x = ⟨u, v (u (A × B) v 𝐶)))
109 elxp 4305 . . . . . . . . 9 (u (A × B) ↔ zw(u = ⟨z, w (z A w B)))
110109anbi1i 431 . . . . . . . 8 ((u (A × B) (x = ⟨u, v v 𝐶)) ↔ (zw(u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)))
111 an12 495 . . . . . . . 8 ((x = ⟨u, v (u (A × B) v 𝐶)) ↔ (u (A × B) (x = ⟨u, v v 𝐶)))
112 19.41vv 1780 . . . . . . . 8 (zw((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)) ↔ (zw(u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)))
113110, 111, 1123bitr4i 201 . . . . . . 7 ((x = ⟨u, v (u (A × B) v 𝐶)) ↔ zw((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)))
1141132exbii 1494 . . . . . 6 (vu(x = ⟨u, v (u (A × B) v 𝐶)) ↔ vuzw((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)))
115 exrot4 1578 . . . . . 6 (vuzw((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)) ↔ zwvu((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)))
116 anass 381 . . . . . . . . 9 (((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)) ↔ (u = ⟨z, w ((z A w B) (x = ⟨u, v v 𝐶))))
117116exbii 1493 . . . . . . . 8 (u((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)) ↔ u(u = ⟨z, w ((z A w B) (x = ⟨u, v v 𝐶))))
118 opeq1 3540 . . . . . . . . . . . 12 (u = ⟨z, w⟩ → ⟨u, v⟩ = ⟨⟨z, w⟩, v⟩)
119118eqeq2d 2048 . . . . . . . . . . 11 (u = ⟨z, w⟩ → (x = ⟨u, v⟩ ↔ x = ⟨⟨z, w⟩, v⟩))
120119anbi1d 438 . . . . . . . . . 10 (u = ⟨z, w⟩ → ((x = ⟨u, v v 𝐶) ↔ (x = ⟨⟨z, w⟩, v v 𝐶)))
121120anbi2d 437 . . . . . . . . 9 (u = ⟨z, w⟩ → (((z A w B) (x = ⟨u, v v 𝐶)) ↔ ((z A w B) (x = ⟨⟨z, w⟩, v v 𝐶))))
12244, 121ceqsexv 2587 . . . . . . . 8 (u(u = ⟨z, w ((z A w B) (x = ⟨u, v v 𝐶))) ↔ ((z A w B) (x = ⟨⟨z, w⟩, v v 𝐶)))
123 an12 495 . . . . . . . 8 (((z A w B) (x = ⟨⟨z, w⟩, v v 𝐶)) ↔ (x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)))
124117, 122, 1233bitri 195 . . . . . . 7 (u((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)) ↔ (x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)))
1251243exbii 1495 . . . . . 6 (zwvu((u = ⟨z, w (z A w B)) (x = ⟨u, v v 𝐶)) ↔ zwv(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)))
126114, 115, 1253bitri 195 . . . . 5 (vu(x = ⟨u, v (u (A × B) v 𝐶)) ↔ zwv(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)))
127107, 108, 1263bitri 195 . . . 4 (x ((A × B) × 𝐶) ↔ zwv(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)))
128127anbi1i 431 . . 3 ((x ((A × B) × 𝐶) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ (zwv(x = ⟨⟨z, w⟩, v ((z A w B) v 𝐶)) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩))
129 elxp 4305 . . . . 5 (y (A × (B × 𝐶)) ↔ zu(y = ⟨z, u (z A u (B × 𝐶))))
130 elxp 4305 . . . . . . . . . 10 (u (B × 𝐶) ↔ wv(u = ⟨w, v (w B v 𝐶)))
131130anbi2i 430 . . . . . . . . 9 (((y = ⟨z, u z A) u (B × 𝐶)) ↔ ((y = ⟨z, u z A) wv(u = ⟨w, v (w B v 𝐶))))
132 anass 381 . . . . . . . . 9 (((y = ⟨z, u z A) u (B × 𝐶)) ↔ (y = ⟨z, u (z A u (B × 𝐶))))
133 19.42vv 1785 . . . . . . . . . 10 (wv((y = ⟨z, u z A) (u = ⟨w, v (w B v 𝐶))) ↔ ((y = ⟨z, u z A) wv(u = ⟨w, v (w B v 𝐶))))
134 an12 495 . . . . . . . . . . . 12 (((y = ⟨z, u z A) (u = ⟨w, v (w B v 𝐶))) ↔ (u = ⟨w, v ((y = ⟨z, u z A) (w B v 𝐶))))
135 anass 381 . . . . . . . . . . . . 13 (((y = ⟨z, u z A) (w B v 𝐶)) ↔ (y = ⟨z, u (z A (w B v 𝐶))))
136135anbi2i 430 . . . . . . . . . . . 12 ((u = ⟨w, v ((y = ⟨z, u z A) (w B v 𝐶))) ↔ (u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
137134, 136bitri 173 . . . . . . . . . . 11 (((y = ⟨z, u z A) (u = ⟨w, v (w B v 𝐶))) ↔ (u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
1381372exbii 1494 . . . . . . . . . 10 (wv((y = ⟨z, u z A) (u = ⟨w, v (w B v 𝐶))) ↔ wv(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
139133, 138bitr3i 175 . . . . . . . . 9 (((y = ⟨z, u z A) wv(u = ⟨w, v (w B v 𝐶))) ↔ wv(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
140131, 132, 1393bitr3i 199 . . . . . . . 8 ((y = ⟨z, u (z A u (B × 𝐶))) ↔ wv(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
141140exbii 1493 . . . . . . 7 (u(y = ⟨z, u (z A u (B × 𝐶))) ↔ uwv(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
142 exrot3 1577 . . . . . . 7 (uwv(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))) ↔ wvu(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))))
143 opeq2 3541 . . . . . . . . . . 11 (u = ⟨w, v⟩ → ⟨z, u⟩ = ⟨z, ⟨w, v⟩⟩)
144143eqeq2d 2048 . . . . . . . . . 10 (u = ⟨w, v⟩ → (y = ⟨z, u⟩ ↔ y = ⟨z, ⟨w, v⟩⟩))
145144anbi1d 438 . . . . . . . . 9 (u = ⟨w, v⟩ → ((y = ⟨z, u (z A (w B v 𝐶))) ↔ (y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶)))))
14669, 145ceqsexv 2587 . . . . . . . 8 (u(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))) ↔ (y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))))
1471462exbii 1494 . . . . . . 7 (wvu(u = ⟨w, v (y = ⟨z, u (z A (w B v 𝐶)))) ↔ wv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))))
148141, 142, 1473bitri 195 . . . . . 6 (u(y = ⟨z, u (z A u (B × 𝐶))) ↔ wv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))))
149148exbii 1493 . . . . 5 (zu(y = ⟨z, u (z A u (B × 𝐶))) ↔ zwv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))))
150129, 149bitri 173 . . . 4 (y (A × (B × 𝐶)) ↔ zwv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))))
151150anbi1i 431 . . 3 ((y (A × (B × 𝐶)) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩) ↔ (zwv(y = ⟨z, ⟨w, v⟩⟩ (z A (w B v 𝐶))) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
152106, 128, 1513bitr4i 201 . 2 ((x ((A × B) × 𝐶) y = ⟨ dom { dom {x}}, ⟨ ran { dom {x}}, ran {x}⟩⟩) ↔ (y (A × (B × 𝐶)) x = ⟨⟨ dom {y}, dom { ran {y}}⟩, ran { ran {y}}⟩))
1535, 7, 21, 35, 152en2i 6186 1 ((A × B) × 𝐶) ≈ (A × (B × 𝐶))
Colors of variables: wff set class
Syntax hints:   wa 97   = wceq 1242  wex 1378   wcel 1390  Vcvv 2551  {csn 3367  cop 3370   cuni 3571   class class class wbr 3755   × cxp 4286  dom cdm 4288  ran crn 4289  cen 6155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-en 6158
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator