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

Theorem xpassen 6732
 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 𝐴 ∈ V
xpassen.2 𝐵 ∈ V
xpassen.3 𝐶 ∈ V
Assertion
Ref Expression
xpassen ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶))

Proof of Theorem xpassen
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpassen.1 . . . 4 𝐴 ∈ V
2 xpassen.2 . . . 4 𝐵 ∈ V
31, 2xpex 4662 . . 3 (𝐴 × 𝐵) ∈ V
4 xpassen.3 . . 3 𝐶 ∈ V
53, 4xpex 4662 . 2 ((𝐴 × 𝐵) × 𝐶) ∈ V
62, 4xpex 4662 . . 3 (𝐵 × 𝐶) ∈ V
71, 6xpex 4662 . 2 (𝐴 × (𝐵 × 𝐶)) ∈ V
8 vex 2692 . . . . . . . . . 10 𝑥 ∈ V
98snex 4117 . . . . . . . . 9 {𝑥} ∈ V
109dmex 4813 . . . . . . . 8 dom {𝑥} ∈ V
1110uniex 4367 . . . . . . 7 dom {𝑥} ∈ V
1211snex 4117 . . . . . 6 { dom {𝑥}} ∈ V
1312dmex 4813 . . . . 5 dom { dom {𝑥}} ∈ V
1413uniex 4367 . . . 4 dom { dom {𝑥}} ∈ V
1512rnex 4814 . . . . . 6 ran { dom {𝑥}} ∈ V
1615uniex 4367 . . . . 5 ran { dom {𝑥}} ∈ V
179rnex 4814 . . . . . 6 ran {𝑥} ∈ V
1817uniex 4367 . . . . 5 ran {𝑥} ∈ V
1916, 18opex 4159 . . . 4 ran { dom {𝑥}}, ran {𝑥}⟩ ∈ V
2014, 19opex 4159 . . 3 dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩ ∈ V
2120a1i 9 . 2 (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) → ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩ ∈ V)
22 vex 2692 . . . . . . . 8 𝑦 ∈ V
2322snex 4117 . . . . . . 7 {𝑦} ∈ V
2423dmex 4813 . . . . . 6 dom {𝑦} ∈ V
2524uniex 4367 . . . . 5 dom {𝑦} ∈ V
2623rnex 4814 . . . . . . . . 9 ran {𝑦} ∈ V
2726uniex 4367 . . . . . . . 8 ran {𝑦} ∈ V
2827snex 4117 . . . . . . 7 { ran {𝑦}} ∈ V
2928dmex 4813 . . . . . 6 dom { ran {𝑦}} ∈ V
3029uniex 4367 . . . . 5 dom { ran {𝑦}} ∈ V
3125, 30opex 4159 . . . 4 dom {𝑦}, dom { ran {𝑦}}⟩ ∈ V
3228rnex 4814 . . . . 5 ran { ran {𝑦}} ∈ V
3332uniex 4367 . . . 4 ran { ran {𝑦}} ∈ V
3431, 33opex 4159 . . 3 ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩ ∈ V
3534a1i 9 . 2 (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) → ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩ ∈ V)
36 sneq 3543 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → {𝑥} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
3736dmeqd 4749 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom {𝑥} = dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
3837unieqd 3755 . . . . . . . . . . . . . . 15 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom {𝑥} = dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
3938sneqd 3545 . . . . . . . . . . . . . 14 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → { dom {𝑥}} = { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
4039dmeqd 4749 . . . . . . . . . . . . 13 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom { dom {𝑥}} = dom { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
4140unieqd 3755 . . . . . . . . . . . 12 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom { dom {𝑥}} = dom { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
42 vex 2692 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
43 vex 2692 . . . . . . . . . . . . . . . . . 18 𝑤 ∈ V
4442, 43opex 4159 . . . . . . . . . . . . . . . . 17 𝑧, 𝑤⟩ ∈ V
45 vex 2692 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
4644, 45op1sta 5028 . . . . . . . . . . . . . . . 16 dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩} = ⟨𝑧, 𝑤
4746sneqi 3544 . . . . . . . . . . . . . . 15 { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = {⟨𝑧, 𝑤⟩}
4847dmeqi 4748 . . . . . . . . . . . . . 14 dom { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = dom {⟨𝑧, 𝑤⟩}
4948unieqi 3754 . . . . . . . . . . . . 13 dom { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = dom {⟨𝑧, 𝑤⟩}
5042, 43op1sta 5028 . . . . . . . . . . . . 13 dom {⟨𝑧, 𝑤⟩} = 𝑧
5149, 50eqtri 2161 . . . . . . . . . . . 12 dom { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = 𝑧
5241, 51eqtr2di 2190 . . . . . . . . . . 11 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑧 = dom { dom {𝑥}})
5339rneqd 4776 . . . . . . . . . . . . . 14 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran { dom {𝑥}} = ran { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
5453unieqd 3755 . . . . . . . . . . . . 13 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran { dom {𝑥}} = ran { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
5547rneqi 4775 . . . . . . . . . . . . . . 15 ran { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ran {⟨𝑧, 𝑤⟩}
5655unieqi 3754 . . . . . . . . . . . . . 14 ran { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ran {⟨𝑧, 𝑤⟩}
5742, 43op2nda 5031 . . . . . . . . . . . . . 14 ran {⟨𝑧, 𝑤⟩} = 𝑤
5856, 57eqtri 2161 . . . . . . . . . . . . 13 ran { dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = 𝑤
5954, 58eqtr2di 2190 . . . . . . . . . . . 12 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑤 = ran { dom {𝑥}})
6036rneqd 4776 . . . . . . . . . . . . . 14 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran {𝑥} = ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
6160unieqd 3755 . . . . . . . . . . . . 13 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran {𝑥} = ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
6244, 45op2nda 5031 . . . . . . . . . . . . 13 ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩} = 𝑣
6361, 62eqtr2di 2190 . . . . . . . . . . . 12 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑣 = ran {𝑥})
6459, 63opeq12d 3721 . . . . . . . . . . 11 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ⟨𝑤, 𝑣⟩ = ⟨ ran { dom {𝑥}}, ran {𝑥}⟩)
6552, 64opeq12d 3721 . . . . . . . . . 10 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩)
66 sneq 3543 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → {𝑦} = {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
6766dmeqd 4749 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom {𝑦} = dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
6867unieqd 3755 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom {𝑦} = dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
6943, 45opex 4159 . . . . . . . . . . . . . 14 𝑤, 𝑣⟩ ∈ V
7042, 69op1sta 5028 . . . . . . . . . . . . 13 dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩} = 𝑧
7168, 70eqtr2di 2190 . . . . . . . . . . . 12 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑧 = dom {𝑦})
7266rneqd 4776 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran {𝑦} = ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
7372unieqd 3755 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran {𝑦} = ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
7473sneqd 3545 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → { ran {𝑦}} = { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
7574dmeqd 4749 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom { ran {𝑦}} = dom { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
7675unieqd 3755 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom { ran {𝑦}} = dom { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
7742, 69op2nda 5031 . . . . . . . . . . . . . . . . 17 ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩} = ⟨𝑤, 𝑣
7877sneqi 3544 . . . . . . . . . . . . . . . 16 { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = {⟨𝑤, 𝑣⟩}
7978dmeqi 4748 . . . . . . . . . . . . . . 15 dom { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = dom {⟨𝑤, 𝑣⟩}
8079unieqi 3754 . . . . . . . . . . . . . 14 dom { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = dom {⟨𝑤, 𝑣⟩}
8143, 45op1sta 5028 . . . . . . . . . . . . . 14 dom {⟨𝑤, 𝑣⟩} = 𝑤
8280, 81eqtri 2161 . . . . . . . . . . . . 13 dom { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = 𝑤
8376, 82eqtr2di 2190 . . . . . . . . . . . 12 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑤 = dom { ran {𝑦}})
8471, 83opeq12d 3721 . . . . . . . . . . 11 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ⟨𝑧, 𝑤⟩ = ⟨ dom {𝑦}, dom { ran {𝑦}}⟩)
8574rneqd 4776 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran { ran {𝑦}} = ran { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
8685unieqd 3755 . . . . . . . . . . . 12 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran { ran {𝑦}} = ran { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
8778rneqi 4775 . . . . . . . . . . . . . 14 ran { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ran {⟨𝑤, 𝑣⟩}
8887unieqi 3754 . . . . . . . . . . . . 13 ran { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ran {⟨𝑤, 𝑣⟩}
8943, 45op2nda 5031 . . . . . . . . . . . . 13 ran {⟨𝑤, 𝑣⟩} = 𝑣
9088, 89eqtri 2161 . . . . . . . . . . . 12 ran { ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = 𝑣
9186, 90eqtr2di 2190 . . . . . . . . . . 11 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑣 = ran { ran {𝑦}})
9284, 91opeq12d 3721 . . . . . . . . . 10 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩)
9365, 92eq2tri 2200 . . . . . . . . 9 ((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
94 anass 399 . . . . . . . . 9 (((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶) ↔ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))
9593, 94anbi12i 456 . . . . . . . 8 (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩) ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
96 an32 552 . . . . . . . 8 (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ ((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)))
97 an32 552 . . . . . . . 8 (((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩) ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
9895, 96, 973bitr4i 211 . . . . . . 7 (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
9998exbii 1585 . . . . . 6 (∃𝑣((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ ∃𝑣((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
100 19.41v 1875 . . . . . 6 (∃𝑣((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩))
101 19.41v 1875 . . . . . 6 (∃𝑣((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩) ↔ (∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
10299, 100, 1013bitr3i 209 . . . . 5 ((∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
1031022exbii 1586 . . . 4 (∃𝑧𝑤(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ ∃𝑧𝑤(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
104 19.41vv 1876 . . . 4 (∃𝑧𝑤(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (∃𝑧𝑤𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩))
105 19.41vv 1876 . . . 4 (∃𝑧𝑤(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩) ↔ (∃𝑧𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
106103, 104, 1053bitr3i 209 . . 3 ((∃𝑧𝑤𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (∃𝑧𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
107 elxp 4564 . . . . 5 (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)))
108 excom 1643 . . . . 5 (∃𝑢𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)) ↔ ∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)))
109 elxp 4564 . . . . . . . . 9 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑧𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)))
110109anbi1i 454 . . . . . . . 8 ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ (∃𝑧𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)))
111 an12 551 . . . . . . . 8 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)))
112 19.41vv 1876 . . . . . . . 8 (∃𝑧𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ (∃𝑧𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)))
113110, 111, 1123bitr4i 211 . . . . . . 7 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)) ↔ ∃𝑧𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)))
1141132exbii 1586 . . . . . 6 (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)) ↔ ∃𝑣𝑢𝑧𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)))
115 exrot4 1670 . . . . . 6 (∃𝑣𝑢𝑧𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ ∃𝑧𝑤𝑣𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)))
116 anass 399 . . . . . . . . 9 (((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ (𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶))))
117116exbii 1585 . . . . . . . 8 (∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ ∃𝑢(𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶))))
118 opeq1 3713 . . . . . . . . . . . 12 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨𝑢, 𝑣⟩ = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩)
119118eqeq2d 2152 . . . . . . . . . . 11 (𝑢 = ⟨𝑧, 𝑤⟩ → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩))
120119anbi1d 461 . . . . . . . . . 10 (𝑢 = ⟨𝑧, 𝑤⟩ → ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣𝐶)))
121120anbi2d 460 . . . . . . . . 9 (𝑢 = ⟨𝑧, 𝑤⟩ → (((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ ((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣𝐶))))
12244, 121ceqsexv 2728 . . . . . . . 8 (∃𝑢(𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶))) ↔ ((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣𝐶)))
123 an12 551 . . . . . . . 8 (((𝑧𝐴𝑤𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣𝐶)) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)))
124117, 122, 1233bitri 205 . . . . . . 7 (∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)))
1251243exbii 1587 . . . . . 6 (∃𝑧𝑤𝑣𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧𝐴𝑤𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣𝐶)) ↔ ∃𝑧𝑤𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)))
126114, 115, 1253bitri 205 . . . . 5 (∃𝑣𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣𝐶)) ↔ ∃𝑧𝑤𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)))
127107, 108, 1263bitri 205 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑧𝑤𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)))
128127anbi1i 454 . . 3 ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (∃𝑧𝑤𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧𝐴𝑤𝐵) ∧ 𝑣𝐶)) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩))
129 elxp 4564 . . . . 5 (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ↔ ∃𝑧𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴𝑢 ∈ (𝐵 × 𝐶))))
130 elxp 4564 . . . . . . . . . 10 (𝑢 ∈ (𝐵 × 𝐶) ↔ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶)))
131130anbi2i 453 . . . . . . . . 9 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ 𝑢 ∈ (𝐵 × 𝐶)) ↔ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))))
132 anass 399 . . . . . . . . 9 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ 𝑢 ∈ (𝐵 × 𝐶)) ↔ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴𝑢 ∈ (𝐵 × 𝐶))))
133 19.42vv 1884 . . . . . . . . . 10 (∃𝑤𝑣((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))) ↔ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))))
134 an12 551 . . . . . . . . . . . 12 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑤𝐵𝑣𝐶))))
135 anass 399 . . . . . . . . . . . . 13 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑤𝐵𝑣𝐶)) ↔ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
136135anbi2i 453 . . . . . . . . . . . 12 ((𝑢 = ⟨𝑤, 𝑣⟩ ∧ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑤𝐵𝑣𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
137134, 136bitri 183 . . . . . . . . . . 11 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
1381372exbii 1586 . . . . . . . . . 10 (∃𝑤𝑣((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))) ↔ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
139133, 138bitr3i 185 . . . . . . . . 9 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧𝐴) ∧ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤𝐵𝑣𝐶))) ↔ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
140131, 132, 1393bitr3i 209 . . . . . . . 8 ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
141140exbii 1585 . . . . . . 7 (∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑢𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
142 exrot3 1669 . . . . . . 7 (∃𝑢𝑤𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))) ↔ ∃𝑤𝑣𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
143 opeq2 3714 . . . . . . . . . . 11 (𝑢 = ⟨𝑤, 𝑣⟩ → ⟨𝑧, 𝑢⟩ = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩)
144143eqeq2d 2152 . . . . . . . . . 10 (𝑢 = ⟨𝑤, 𝑣⟩ → (𝑦 = ⟨𝑧, 𝑢⟩ ↔ 𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩))
145144anbi1d 461 . . . . . . . . 9 (𝑢 = ⟨𝑤, 𝑣⟩ → ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))))
14669, 145ceqsexv 2728 . . . . . . . 8 (∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
1471462exbii 1586 . . . . . . 7 (∃𝑤𝑣𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶)))) ↔ ∃𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
148141, 142, 1473bitri 205 . . . . . 6 (∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
149148exbii 1585 . . . . 5 (∃𝑧𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧𝐴𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑧𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
150129, 149bitri 183 . . . 4 (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ↔ ∃𝑧𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))))
151150anbi1i 454 . . 3 ((𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩) ↔ (∃𝑧𝑤𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧𝐴 ∧ (𝑤𝐵𝑣𝐶))) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
152106, 128, 1513bitr4i 211 . 2 ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 = ⟨ dom { dom {𝑥}}, ⟨ ran { dom {𝑥}}, ran {𝑥}⟩⟩) ↔ (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ∧ 𝑥 = ⟨⟨ dom {𝑦}, dom { ran {𝑦}}⟩, ran { ran {𝑦}}⟩))
1535, 7, 21, 35, 152en2i 6672 1 ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   = wceq 1332  ∃wex 1469   ∈ wcel 1481  Vcvv 2689  {csn 3532  ⟨cop 3535  ∪ cuni 3744   class class class wbr 3937   × cxp 4545  dom cdm 4547  ran crn 4548   ≈ cen 6640 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-opab 3998  df-mpt 3999  df-id 4223  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-en 6643 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator