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 ( ( 𝐴 × 𝐵 ) × 𝐶 ) ≈ ( 𝐴 × ( 𝐵 × 𝐶 ) )