This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- A e. _V
xpassen.2 
|- B e. _V
xpassen.3 
|- C e. _V
Assertion xpassen 
|- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )

Proof

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