MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpassen Structured version   Visualization version   GIF version
Theorem xpassen 8806
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 7581 . . 3 (𝐴 × 𝐵) ∈ V
4 xpassen.3 . . 3 𝐶 ∈ V
53, 4xpex 7581 . 2 ((𝐴 × 𝐵) × 𝐶) ∈ V
62, 4xpex 7581 . . 3 (𝐵 × 𝐶) ∈ V
71, 6xpex 7581 . 2 (𝐴 × (𝐵 × 𝐶)) ∈ V
8 opex 5373 . . 3 ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩ ∈ V
98a1i 11 . 2 (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) → ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩ ∈ V)
10 opex 5373 . . 3 ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩ ∈ V
1110a1i 11 . 2 (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) → ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩ ∈ V)
12 sneq 4568 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → {𝑥} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
1312dmeqd 5803 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom {𝑥} = dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
1413unieqd 4850 . . . . . . . . . . . . . . 15 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪ dom {𝑥} = ∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
1514sneqd 4570 . . . . . . . . . . . . . 14 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → {∪ dom {𝑥}} = {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
1615dmeqd 5803 . . . . . . . . . . . . 13 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom {∪ dom {𝑥}} = dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
1716unieqd 4850 . . . . . . . . . . . 12 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪ dom {∪ dom {𝑥}} = ∪ dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
18 opex 5373 . . . . . . . . . . . . . . . . 17 ⟨𝑧, 𝑤⟩ ∈ V
19 vex 3426 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
2018, 19op1sta 6117 . . . . . . . . . . . . . . . 16 ∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩} = ⟨𝑧, 𝑤⟩
2120sneqi 4569 . . . . . . . . . . . . . . 15 {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = {⟨𝑧, 𝑤⟩}
2221dmeqi 5802 . . . . . . . . . . . . . 14 dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = dom {⟨𝑧, 𝑤⟩}
2322unieqi 4849 . . . . . . . . . . . . 13 ∪ dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ∪ dom {⟨𝑧, 𝑤⟩}
24 vex 3426 . . . . . . . . . . . . . 14 𝑧 ∈ V
25 vex 3426 . . . . . . . . . . . . . 14 𝑤 ∈ V
2624, 25op1sta 6117 . . . . . . . . . . . . 13 ∪ dom {⟨𝑧, 𝑤⟩} = 𝑧
2723, 26eqtri 2766 . . . . . . . . . . . 12 ∪ dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = 𝑧
2817, 27eqtr2di 2796 . . . . . . . . . . 11 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑧 = ∪ dom {∪ dom {𝑥}})
2915rneqd 5836 . . . . . . . . . . . . . 14 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran {∪ dom {𝑥}} = ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
3029unieqd 4850 . . . . . . . . . . . . 13 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪ ran {∪ dom {𝑥}} = ∪ ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}})
3121rneqi 5835 . . . . . . . . . . . . . . 15 ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ran {⟨𝑧, 𝑤⟩}
3231unieqi 4849 . . . . . . . . . . . . . 14 ∪ ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ∪ ran {⟨𝑧, 𝑤⟩}
3324, 25op2nda 6120 . . . . . . . . . . . . . 14 ∪ ran {⟨𝑧, 𝑤⟩} = 𝑤
3432, 33eqtri 2766 . . . . . . . . . . . . 13 ∪ ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = 𝑤
3530, 34eqtr2di 2796 . . . . . . . . . . . 12 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑤 = ∪ ran {∪ dom {𝑥}})
3612rneqd 5836 . . . . . . . . . . . . . 14 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran {𝑥} = ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
3736unieqd 4850 . . . . . . . . . . . . 13 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪ ran {𝑥} = ∪ ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩})
3818, 19op2nda 6120 . . . . . . . . . . . . 13 ∪ ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩} = 𝑣
3937, 38eqtr2di 2796 . . . . . . . . . . . 12 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑣 = ∪ ran {𝑥})
4035, 39opeq12d 4809 . . . . . . . . . . 11 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ⟨𝑤, 𝑣⟩ = ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩)
4128, 40opeq12d 4809 . . . . . . . . . 10 (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩)
42 sneq 4568 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → {𝑦} = {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
4342dmeqd 5803 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom {𝑦} = dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
4443unieqd 4850 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ dom {𝑦} = ∪ dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
45 opex 5373 . . . . . . . . . . . . . 14 ⟨𝑤, 𝑣⟩ ∈ V
4624, 45op1sta 6117 . . . . . . . . . . . . 13 ∪ dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩} = 𝑧
4744, 46eqtr2di 2796 . . . . . . . . . . . 12 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑧 = ∪ dom {𝑦})
4842rneqd 5836 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran {𝑦} = ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
4948unieqd 4850 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ ran {𝑦} = ∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩})
5049sneqd 4570 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → {∪ ran {𝑦}} = {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
5150dmeqd 5803 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom {∪ ran {𝑦}} = dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
5251unieqd 4850 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ dom {∪ ran {𝑦}} = ∪ dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
5324, 45op2nda 6120 . . . . . . . . . . . . . . . . 17 ∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩} = ⟨𝑤, 𝑣⟩
5453sneqi 4569 . . . . . . . . . . . . . . . 16 {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = {⟨𝑤, 𝑣⟩}
5554dmeqi 5802 . . . . . . . . . . . . . . 15 dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = dom {⟨𝑤, 𝑣⟩}
5655unieqi 4849 . . . . . . . . . . . . . 14 ∪ dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ∪ dom {⟨𝑤, 𝑣⟩}
5725, 19op1sta 6117 . . . . . . . . . . . . . 14 ∪ dom {⟨𝑤, 𝑣⟩} = 𝑤
5856, 57eqtri 2766 . . . . . . . . . . . . 13 ∪ dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = 𝑤
5952, 58eqtr2di 2796 . . . . . . . . . . . 12 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑤 = ∪ dom {∪ ran {𝑦}})
6047, 59opeq12d 4809 . . . . . . . . . . 11 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ⟨𝑧, 𝑤⟩ = ⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩)
6150rneqd 5836 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran {∪ ran {𝑦}} = ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
6261unieqd 4850 . . . . . . . . . . . 12 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ ran {∪ ran {𝑦}} = ∪ ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}})
6354rneqi 5835 . . . . . . . . . . . . . 14 ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ran {⟨𝑤, 𝑣⟩}
6463unieqi 4849 . . . . . . . . . . . . 13 ∪ ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ∪ ran {⟨𝑤, 𝑣⟩}
6525, 19op2nda 6120 . . . . . . . . . . . . 13 ∪ ran {⟨𝑤, 𝑣⟩} = 𝑣
6664, 65eqtri 2766 . . . . . . . . . . . 12 ∪ ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = 𝑣
6762, 66eqtr2di 2796 . . . . . . . . . . 11 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑣 = ∪ ran {∪ ran {𝑦}})
6860, 67opeq12d 4809 . . . . . . . . . 10 (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)
6941, 68eq2tri 2806 . . . . . . . . 9 ((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
70 anass 468 . . . . . . . . 9 (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶) ↔ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))
7169, 70anbi12i 626 . . . . . . . 8 (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
72 an32 642 . . . . . . . 8 (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ ((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)))
73 an32 642 . . . . . . . 8 (((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
7471, 72, 733bitr4i 302 . . . . . . 7 (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
7574exbii 1851 . . . . . 6 (∃𝑣((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ ∃𝑣((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
76 19.41v 1954 . . . . . 6 (∃𝑣((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩))
77 19.41v 1954 . . . . . 6 (∃𝑣((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ (∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
7875, 76, 773bitr3i 300 . . . . 5 ((∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
79782exbii 1852 . . . 4 (∃𝑧∃𝑤(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ ∃𝑧∃𝑤(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
80 19.41vv 1955 . . . 4 (∃𝑧∃𝑤(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩))
81 19.41vv 1955 . . . 4 (∃𝑧∃𝑤(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
8279, 80, 813bitr3i 300 . . 3 ((∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
83 elxp 5603 . . . . 5 (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)))
84 excom 2164 . . . . 5 (∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)))
85 elxp 5603 . . . . . . . . 9 (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑧∃𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)))
8685anbi1i 623 . . . . . . . 8 ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (∃𝑧∃𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
87 an12 641 . . . . . . . 8 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
88 19.41vv 1955 . . . . . . . 8 (∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (∃𝑧∃𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
8986, 87, 883bitr4i 302 . . . . . . 7 ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
90892exbii 1852 . . . . . 6 (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑣∃𝑢∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
91 exrot4 2168 . . . . . 6 (∃𝑣∃𝑢∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
92 anass 468 . . . . . . . . 9 (((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))))
9392exbii 1851 . . . . . . . 8 (∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑢(𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))))
94 opeq1 4801 . . . . . . . . . . . 12 (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨𝑢, 𝑣⟩ = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩)
9594eqeq2d 2749 . . . . . . . . . . 11 (𝑢 = ⟨𝑧, 𝑤⟩ → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩))
9695anbi1d 629 . . . . . . . . . 10 (𝑢 = ⟨𝑧, 𝑤⟩ → ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
9796anbi2d 628 . . . . . . . . 9 (𝑢 = ⟨𝑧, 𝑤⟩ → (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))))
9818, 97ceqsexv 3469 . . . . . . . 8 (∃𝑢(𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))
99 an12 641 . . . . . . . 8 (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)))
10093, 98, 993bitri 296 . . . . . . 7 (∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)))
1011003exbii 1853 . . . . . 6 (∃𝑧∃𝑤∃𝑣∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)))
10290, 91, 1013bitri 296 . . . . 5 (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)))
10383, 84, 1023bitri 296 . . . 4 (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)))
104103anbi1i 623 . . 3 ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩))
105 elxp 5603 . . . . 5 (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ↔ ∃𝑧∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))))
106 elxp 5603 . . . . . . . . . 10 (𝑢 ∈ (𝐵 × 𝐶) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))
107106anbi2i 622 . . . . . . . . 9 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ 𝑢 ∈ (𝐵 × 𝐶)) ↔ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
108 anass 468 . . . . . . . . 9 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ 𝑢 ∈ (𝐵 × 𝐶)) ↔ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))))
109 19.42vv 1962 . . . . . . . . . 10 (∃𝑤∃𝑣((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
110 an12 641 . . . . . . . . . . . 12 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
111 anass 468 . . . . . . . . . . . . 13 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)) ↔ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
112111anbi2i 622 . . . . . . . . . . . 12 ((𝑢 = ⟨𝑤, 𝑣⟩ ∧ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
113110, 112bitri 274 . . . . . . . . . . 11 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
1141132exbii 1852 . . . . . . . . . 10 (∃𝑤∃𝑣((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
115109, 114bitr3i 276 . . . . . . . . 9 (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
116107, 108, 1153bitr3i 300 . . . . . . . 8 ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
117116exbii 1851 . . . . . . 7 (∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑢∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
118 exrot3 2167 . . . . . . 7 (∃𝑢∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) ↔ ∃𝑤∃𝑣∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
119 opeq2 4802 . . . . . . . . . . 11 (𝑢 = ⟨𝑤, 𝑣⟩ → ⟨𝑧, 𝑢⟩ = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩)
120119eqeq2d 2749 . . . . . . . . . 10 (𝑢 = ⟨𝑤, 𝑣⟩ → (𝑦 = ⟨𝑧, 𝑢⟩ ↔ 𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩))
121120anbi1d 629 . . . . . . . . 9 (𝑢 = ⟨𝑤, 𝑣⟩ → ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))))
12245, 121ceqsexv 3469 . . . . . . . 8 (∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
1231222exbii 1852 . . . . . . 7 (∃𝑤∃𝑣∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) ↔ ∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
124117, 118, 1233bitri 296 . . . . . 6 (∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
125124exbii 1851 . . . . 5 (∃𝑧∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
126105, 125bitri 274 . . . 4 (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))
127126anbi1i 623 . . 3 ((𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
12882, 104, 1273bitr4i 302 . 2 ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ∧ 𝑥 = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩))
1295, 7, 9, 11, 128en2i 8733 1 ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422  {csn 4558  ⟨cop 4564  ∪ cuni 4836   class class class wbr 5070   × cxp 5578  dom cdm 5580  ran crn 5581   ≈ cen 8688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-en 8692
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator