Metamath Proof Explorer

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

Proof

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