Step | Hyp | Ref
| Expression |
1 | | xpassen.1 |
. . . 4
|
2 | | xpassen.2 |
. . . 4
|
3 | 1, 2 | xpex 4724 |
. . 3
|
4 | | xpassen.3 |
. . 3
|
5 | 3, 4 | xpex 4724 |
. 2
|
6 | 2, 4 | xpex 4724 |
. . 3
|
7 | 1, 6 | xpex 4724 |
. 2
|
8 | | vex 2733 |
. . . . . . . . . 10
|
9 | 8 | snex 4169 |
. . . . . . . . 9
|
10 | 9 | dmex 4875 |
. . . . . . . 8
|
11 | 10 | uniex 4420 |
. . . . . . 7
|
12 | 11 | snex 4169 |
. . . . . 6
|
13 | 12 | dmex 4875 |
. . . . 5
|
14 | 13 | uniex 4420 |
. . . 4
|
15 | 12 | rnex 4876 |
. . . . . 6
|
16 | 15 | uniex 4420 |
. . . . 5
|
17 | 9 | rnex 4876 |
. . . . . 6
|
18 | 17 | uniex 4420 |
. . . . 5
|
19 | 16, 18 | opex 4212 |
. . . 4
|
20 | 14, 19 | opex 4212 |
. . 3
|
21 | 20 | a1i 9 |
. 2
|
22 | | vex 2733 |
. . . . . . . 8
|
23 | 22 | snex 4169 |
. . . . . . 7
|
24 | 23 | dmex 4875 |
. . . . . 6
|
25 | 24 | uniex 4420 |
. . . . 5
|
26 | 23 | rnex 4876 |
. . . . . . . . 9
|
27 | 26 | uniex 4420 |
. . . . . . . 8
|
28 | 27 | snex 4169 |
. . . . . . 7
|
29 | 28 | dmex 4875 |
. . . . . 6
|
30 | 29 | uniex 4420 |
. . . . 5
|
31 | 25, 30 | opex 4212 |
. . . 4
|
32 | 28 | rnex 4876 |
. . . . 5
|
33 | 32 | uniex 4420 |
. . . 4
|
34 | 31, 33 | opex 4212 |
. . 3
|
35 | 34 | a1i 9 |
. 2
|
36 | | sneq 3592 |
. . . . . . . . . . . . . . . . 17
|
37 | 36 | dmeqd 4811 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | unieqd 3805 |
. . . . . . . . . . . . . . 15
|
39 | 38 | sneqd 3594 |
. . . . . . . . . . . . . 14
|
40 | 39 | dmeqd 4811 |
. . . . . . . . . . . . 13
|
41 | 40 | unieqd 3805 |
. . . . . . . . . . . 12
|
42 | | vex 2733 |
. . . . . . . . . . . . . . . . . 18
|
43 | | vex 2733 |
. . . . . . . . . . . . . . . . . 18
|
44 | 42, 43 | opex 4212 |
. . . . . . . . . . . . . . . . 17
|
45 | | vex 2733 |
. . . . . . . . . . . . . . . . 17
|
46 | 44, 45 | op1sta 5090 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | sneqi 3593 |
. . . . . . . . . . . . . . 15
|
48 | 47 | dmeqi 4810 |
. . . . . . . . . . . . . 14
|
49 | 48 | unieqi 3804 |
. . . . . . . . . . . . 13
|
50 | 42, 43 | op1sta 5090 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | eqtri 2191 |
. . . . . . . . . . . 12
|
52 | 41, 51 | eqtr2di 2220 |
. . . . . . . . . . 11
|
53 | 39 | rneqd 4838 |
. . . . . . . . . . . . . 14
|
54 | 53 | unieqd 3805 |
. . . . . . . . . . . . 13
|
55 | 47 | rneqi 4837 |
. . . . . . . . . . . . . . 15
|
56 | 55 | unieqi 3804 |
. . . . . . . . . . . . . 14
|
57 | 42, 43 | op2nda 5093 |
. . . . . . . . . . . . . 14
|
58 | 56, 57 | eqtri 2191 |
. . . . . . . . . . . . 13
|
59 | 54, 58 | eqtr2di 2220 |
. . . . . . . . . . . 12
|
60 | 36 | rneqd 4838 |
. . . . . . . . . . . . . 14
|
61 | 60 | unieqd 3805 |
. . . . . . . . . . . . 13
|
62 | 44, 45 | op2nda 5093 |
. . . . . . . . . . . . 13
|
63 | 61, 62 | eqtr2di 2220 |
. . . . . . . . . . . 12
|
64 | 59, 63 | opeq12d 3771 |
. . . . . . . . . . 11
|
65 | 52, 64 | opeq12d 3771 |
. . . . . . . . . 10
|
66 | | sneq 3592 |
. . . . . . . . . . . . . . 15
|
67 | 66 | dmeqd 4811 |
. . . . . . . . . . . . . 14
|
68 | 67 | unieqd 3805 |
. . . . . . . . . . . . 13
|
69 | 43, 45 | opex 4212 |
. . . . . . . . . . . . . 14
|
70 | 42, 69 | op1sta 5090 |
. . . . . . . . . . . . 13
|
71 | 68, 70 | eqtr2di 2220 |
. . . . . . . . . . . 12
|
72 | 66 | rneqd 4838 |
. . . . . . . . . . . . . . . . 17
|
73 | 72 | unieqd 3805 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | sneqd 3594 |
. . . . . . . . . . . . . . 15
|
75 | 74 | dmeqd 4811 |
. . . . . . . . . . . . . 14
|
76 | 75 | unieqd 3805 |
. . . . . . . . . . . . 13
|
77 | 42, 69 | op2nda 5093 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | sneqi 3593 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | dmeqi 4810 |
. . . . . . . . . . . . . . 15
|
80 | 79 | unieqi 3804 |
. . . . . . . . . . . . . 14
|
81 | 43, 45 | op1sta 5090 |
. . . . . . . . . . . . . 14
|
82 | 80, 81 | eqtri 2191 |
. . . . . . . . . . . . 13
|
83 | 76, 82 | eqtr2di 2220 |
. . . . . . . . . . . 12
|
84 | 71, 83 | opeq12d 3771 |
. . . . . . . . . . 11
|
85 | 74 | rneqd 4838 |
. . . . . . . . . . . . 13
|
86 | 85 | unieqd 3805 |
. . . . . . . . . . . 12
|
87 | 78 | rneqi 4837 |
. . . . . . . . . . . . . 14
|
88 | 87 | unieqi 3804 |
. . . . . . . . . . . . 13
|
89 | 43, 45 | op2nda 5093 |
. . . . . . . . . . . . 13
|
90 | 88, 89 | eqtri 2191 |
. . . . . . . . . . . 12
|
91 | 86, 90 | eqtr2di 2220 |
. . . . . . . . . . 11
|
92 | 84, 91 | opeq12d 3771 |
. . . . . . . . . 10
|
93 | 65, 92 | eq2tri 2230 |
. . . . . . . . 9
|
94 | | anass 399 |
. . . . . . . . 9
|
95 | 93, 94 | anbi12i 457 |
. . . . . . . 8
|
96 | | an32 557 |
. . . . . . . 8
|
97 | | an32 557 |
. . . . . . . 8
|
98 | 95, 96, 97 | 3bitr4i 211 |
. . . . . . 7
|
99 | 98 | exbii 1598 |
. . . . . 6
|
100 | | 19.41v 1895 |
. . . . . 6
|
101 | | 19.41v 1895 |
. . . . . 6
|
102 | 99, 100, 101 | 3bitr3i 209 |
. . . . 5
|
103 | 102 | 2exbii 1599 |
. . . 4
|
104 | | 19.41vv 1896 |
. . . 4
|
105 | | 19.41vv 1896 |
. . . 4
|
106 | 103, 104,
105 | 3bitr3i 209 |
. . 3
|
107 | | elxp 4626 |
. . . . 5
|
108 | | excom 1657 |
. . . . 5
|
109 | | elxp 4626 |
. . . . . . . . 9
|
110 | 109 | anbi1i 455 |
. . . . . . . 8
|
111 | | an12 556 |
. . . . . . . 8
|
112 | | 19.41vv 1896 |
. . . . . . . 8
|
113 | 110, 111,
112 | 3bitr4i 211 |
. . . . . . 7
|
114 | 113 | 2exbii 1599 |
. . . . . 6
|
115 | | exrot4 1684 |
. . . . . 6
|
116 | | anass 399 |
. . . . . . . . 9
|
117 | 116 | exbii 1598 |
. . . . . . . 8
|
118 | | opeq1 3763 |
. . . . . . . . . . . 12
|
119 | 118 | eqeq2d 2182 |
. . . . . . . . . . 11
|
120 | 119 | anbi1d 462 |
. . . . . . . . . 10
|
121 | 120 | anbi2d 461 |
. . . . . . . . 9
|
122 | 44, 121 | ceqsexv 2769 |
. . . . . . . 8
|
123 | | an12 556 |
. . . . . . . 8
|
124 | 117, 122,
123 | 3bitri 205 |
. . . . . . 7
|
125 | 124 | 3exbii 1600 |
. . . . . 6
|
126 | 114, 115,
125 | 3bitri 205 |
. . . . 5
|
127 | 107, 108,
126 | 3bitri 205 |
. . . 4
|
128 | 127 | anbi1i 455 |
. . 3
|
129 | | elxp 4626 |
. . . . 5
|
130 | | elxp 4626 |
. . . . . . . . . 10
|
131 | 130 | anbi2i 454 |
. . . . . . . . 9
|
132 | | anass 399 |
. . . . . . . . 9
|
133 | | 19.42vv 1904 |
. . . . . . . . . 10
|
134 | | an12 556 |
. . . . . . . . . . . 12
|
135 | | anass 399 |
. . . . . . . . . . . . 13
|
136 | 135 | anbi2i 454 |
. . . . . . . . . . . 12
|
137 | 134, 136 | bitri 183 |
. . . . . . . . . . 11
|
138 | 137 | 2exbii 1599 |
. . . . . . . . . 10
|
139 | 133, 138 | bitr3i 185 |
. . . . . . . . 9
|
140 | 131, 132,
139 | 3bitr3i 209 |
. . . . . . . 8
|
141 | 140 | exbii 1598 |
. . . . . . 7
|
142 | | exrot3 1683 |
. . . . . . 7
|
143 | | opeq2 3764 |
. . . . . . . . . . 11
|
144 | 143 | eqeq2d 2182 |
. . . . . . . . . 10
|
145 | 144 | anbi1d 462 |
. . . . . . . . 9
|
146 | 69, 145 | ceqsexv 2769 |
. . . . . . . 8
|
147 | 146 | 2exbii 1599 |
. . . . . . 7
|
148 | 141, 142,
147 | 3bitri 205 |
. . . . . 6
|
149 | 148 | exbii 1598 |
. . . . 5
|
150 | 129, 149 | bitri 183 |
. . . 4
|
151 | 150 | anbi1i 455 |
. . 3
|
152 | 106, 128,
151 | 3bitr4i 211 |
. 2
|
153 | 5, 7, 21, 35, 152 | en2i 6746 |
1
|