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 V
xpassen.2 B V
xpassen.3 C V
Assertion xpassen A × B × C A × B × C

Proof

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