Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . . . 8
|
2 | 1 | elcompl 3225 |
. . . . . . 7
∼ ∼
∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn
∼ ∼
Ins3k Sk Ins2k Sk k1 1 1c k k Nn |
3 | 1 | elimak 4259 |
. . . . . . . . 9
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn
Nn ∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k |
4 | | opkex 4113 |
. . . . . . . . . . . 12
|
5 | 4 | elcompl 3225 |
. . . . . . . . . . 11
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k ∼ Ins3k Sk Ins2k Sk k1 1 1c k |
6 | | elun 3220 |
. . . . . . . . . . . 12
∼
Ins3k Sk Ins2k Sk k1 1 1c k ∼
Ins3k Sk Ins2k Sk k1 1 1c k |
7 | | vex 2862 |
. . . . . . . . . . . . . . . 16
|
8 | 7, 1 | ndisjrelk 4323 |
. . . . . . . . . . . . . . 15
Ins3k Sk Ins2k Sk k1 1 1c |
9 | 8 | notbii 287 |
. . . . . . . . . . . . . 14
Ins3k Sk Ins2k Sk k1 1 1c
|
10 | 4 | elcompl 3225 |
. . . . . . . . . . . . . 14
∼ Ins3k Sk Ins2k Sk k1 1 1c Ins3k Sk Ins2k Sk k1 1 1c |
11 | | df-ne 2518 |
. . . . . . . . . . . . . . 15
|
12 | 11 | con2bii 322 |
. . . . . . . . . . . . . 14
|
13 | 9, 10, 12 | 3bitr4i 268 |
. . . . . . . . . . . . 13
∼ Ins3k Sk Ins2k Sk k1 1 1c
|
14 | | opkelidkg 4274 |
. . . . . . . . . . . . . 14
k |
15 | 7, 1, 14 | mp2an 653 |
. . . . . . . . . . . . 13
k |
16 | 13, 15 | orbi12i 507 |
. . . . . . . . . . . 12
∼
Ins3k Sk Ins2k Sk k1 1 1c k
|
17 | | incom 3448 |
. . . . . . . . . . . . . 14
|
18 | 17 | eqeq1i 2360 |
. . . . . . . . . . . . 13
|
19 | | eqcom 2355 |
. . . . . . . . . . . . 13
|
20 | 18, 19 | orbi12i 507 |
. . . . . . . . . . . 12
|
21 | 6, 16, 20 | 3bitri 262 |
. . . . . . . . . . 11
∼
Ins3k Sk Ins2k Sk k1 1 1c k
|
22 | 5, 21 | xchbinx 301 |
. . . . . . . . . 10
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k
|
23 | 22 | rexbii 2639 |
. . . . . . . . 9
Nn ∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k Nn
|
24 | | rexnal 2625 |
. . . . . . . . 9
Nn
Nn
|
25 | 3, 23, 24 | 3bitri 262 |
. . . . . . . 8
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn Nn
|
26 | 25 | con2bii 322 |
. . . . . . 7
Nn
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn |
27 | 2, 26 | bitr4i 243 |
. . . . . 6
∼ ∼
∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn
Nn
|
28 | 27 | abbi2i 2464 |
. . . . 5
∼ ∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn
Nn
|
29 | | ssetkex 4294 |
. . . . . . . . . . . . 13
Sk |
30 | 29 | ins3kex 4308 |
. . . . . . . . . . . 12
Ins3k Sk |
31 | 29 | ins2kex 4307 |
. . . . . . . . . . . 12
Ins2k Sk |
32 | 30, 31 | inex 4105 |
. . . . . . . . . . 11
Ins3k Sk Ins2k Sk
|
33 | | 1cex 4142 |
. . . . . . . . . . . . 13
1c
|
34 | 33 | pw1ex 4303 |
. . . . . . . . . . . 12
1
1c
|
35 | 34 | pw1ex 4303 |
. . . . . . . . . . 11
1 1
1c
|
36 | 32, 35 | imakex 4300 |
. . . . . . . . . 10
Ins3k Sk Ins2k Sk k1 1 1c
|
37 | 36 | complex 4104 |
. . . . . . . . 9
∼ Ins3k Sk Ins2k Sk k1 1 1c
|
38 | | idkex 4314 |
. . . . . . . . 9
k
|
39 | 37, 38 | unex 4106 |
. . . . . . . 8
∼ Ins3k Sk Ins2k Sk k1 1 1c k |
40 | 39 | complex 4104 |
. . . . . . 7
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k |
41 | | nncex 4396 |
. . . . . . 7
Nn |
42 | 40, 41 | imakex 4300 |
. . . . . 6
∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn |
43 | 42 | complex 4104 |
. . . . 5
∼ ∼ ∼ Ins3k Sk Ins2k Sk k1 1 1c k k Nn |
44 | 28, 43 | eqeltrri 2424 |
. . . 4
Nn
|
45 | | df-0c 4377 |
. . . . . . . . . . 11
0c
|
46 | 45 | eqeq2i 2363 |
. . . . . . . . . 10
0c
|
47 | 46 | biimpi 186 |
. . . . . . . . 9
0c |
48 | 47 | ineq1d 3456 |
. . . . . . . 8
0c
|
49 | 48 | eqeq1d 2361 |
. . . . . . 7
0c
|
50 | | incom 3448 |
. . . . . . . . 9
|
51 | 50 | eqeq1i 2360 |
. . . . . . . 8
|
52 | | disjsn 3786 |
. . . . . . . 8
|
53 | 51, 52 | bitri 240 |
. . . . . . 7
|
54 | 49, 53 | syl6bb 252 |
. . . . . 6
0c
|
55 | | eqeq1 2359 |
. . . . . . 7
0c 0c |
56 | | eqcom 2355 |
. . . . . . 7
0c
0c |
57 | 55, 56 | syl6bb 252 |
. . . . . 6
0c
0c |
58 | 54, 57 | orbi12d 690 |
. . . . 5
0c
0c |
59 | 58 | ralbidv 2634 |
. . . 4
0c Nn
Nn
0c |
60 | | ineq1 3450 |
. . . . . . . 8
|
61 | 60 | eqeq1d 2361 |
. . . . . . 7
|
62 | | eqeq1 2359 |
. . . . . . 7
|
63 | 61, 62 | orbi12d 690 |
. . . . . 6
|
64 | 63 | ralbidv 2634 |
. . . . 5
Nn
Nn
|
65 | | ineq2 3451 |
. . . . . . . 8
|
66 | 65 | eqeq1d 2361 |
. . . . . . 7
|
67 | | equequ2 1686 |
. . . . . . 7
|
68 | 66, 67 | orbi12d 690 |
. . . . . 6
|
69 | 68 | cbvralv 2835 |
. . . . 5
Nn
Nn
|
70 | 64, 69 | syl6bb 252 |
. . . 4
Nn
Nn
|
71 | | ineq1 3450 |
. . . . . . 7
1c
1c |
72 | 71 | eqeq1d 2361 |
. . . . . 6
1c
1c
|
73 | | eqeq1 2359 |
. . . . . 6
1c
1c
|
74 | 72, 73 | orbi12d 690 |
. . . . 5
1c
1c 1c |
75 | 74 | ralbidv 2634 |
. . . 4
1c Nn
Nn 1c
1c
|
76 | | ineq1 3450 |
. . . . . . 7
|
77 | 76 | eqeq1d 2361 |
. . . . . 6
|
78 | | eqeq1 2359 |
. . . . . 6
|
79 | 77, 78 | orbi12d 690 |
. . . . 5
|
80 | 79 | ralbidv 2634 |
. . . 4
Nn
Nn
|
81 | | nnc0suc 4412 |
. . . . . . 7
Nn
0c Nn
1c |
82 | | 0nelsuc 4400 |
. . . . . . . . . . . 12
1c |
83 | | eleq2 2414 |
. . . . . . . . . . . . 13
1c
1c |
84 | 83 | biimpcd 215 |
. . . . . . . . . . . 12
1c
1c |
85 | 82, 84 | mtoi 169 |
. . . . . . . . . . 11
1c |
86 | 85 | adantr 451 |
. . . . . . . . . 10
Nn
1c |
87 | 86 | nrexdv 2717 |
. . . . . . . . 9
Nn 1c |
88 | | orel2 372 |
. . . . . . . . 9
Nn 1c 0c Nn 1c
0c |
89 | 87, 88 | syl 15 |
. . . . . . . 8
0c
Nn
1c 0c |
90 | 89 | com12 27 |
. . . . . . 7
0c Nn
1c
0c |
91 | 81, 90 | sylbi 187 |
. . . . . 6
Nn
0c |
92 | | imor 401 |
. . . . . 6
0c
0c |
93 | 91, 92 | sylib 188 |
. . . . 5
Nn
0c |
94 | 93 | rgen 2679 |
. . . 4
Nn
0c |
95 | | neq0 3560 |
. . . . . . . . 9
1c
1c
|
96 | | elin 3219 |
. . . . . . . . . . 11
1c 1c
|
97 | | elsuc 4413 |
. . . . . . . . . . . . 13
1c
∼ |
98 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
|
99 | 98 | elcompl 3225 |
. . . . . . . . . . . . . . . 16
∼ |
100 | 99 | anbi2i 675 |
. . . . . . . . . . . . . . 15
∼
|
101 | | simp1r 980 |
. . . . . . . . . . . . . . . . . . 19
Nn Nn Nn
Nn |
102 | | nnc0suc 4412 |
. . . . . . . . . . . . . . . . . . 19
Nn
0c Nn
1c |
103 | 101, 102 | sylib 188 |
. . . . . . . . . . . . . . . . . 18
Nn Nn Nn
0c Nn
1c |
104 | | ssun2 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
105 | 98 | snid 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
106 | 104, 105 | sselii 3270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
107 | | n0i 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
109 | 45 | eleq2i 2417 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
0c
|
110 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
111 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
112 | 110, 111 | unex 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
113 | 112 | elsnc 3756 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
114 | 109, 113 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
0c
|
115 | 108, 114 | mtbir 290 |
. . . . . . . . . . . . . . . . . . . . . . 23
0c |
116 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
0c 0c |
117 | 116 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . . . 23
0c
0c |
118 | 115, 117 | mtoi 169 |
. . . . . . . . . . . . . . . . . . . . . 22
0c |
119 | 118 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . 21
Nn Nn Nn
0c |
120 | | orel1 371 |
. . . . . . . . . . . . . . . . . . . . 21
0c 0c Nn 1c
Nn
1c |
121 | 119, 120 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
Nn Nn Nn
0c
Nn 1c
Nn
1c |
122 | | simpll 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn Nn Nn Nn
1c
Nn |
123 | | simpr3r 1017 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Nn Nn Nn Nn
|
124 | 123 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn Nn Nn Nn
1c
|
125 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn Nn Nn Nn
1c
1c |
126 | 110, 98 | nnsucelr 4428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn
1c |
127 | 122, 124,
125, 126 | syl12anc 1180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nn Nn Nn Nn
1c
|
128 | 127 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Nn Nn Nn Nn
1c |
129 | | ineq2 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
130 | 129 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
131 | | equequ2 1686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
132 | 130, 131 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
133 | 132 | rspccv 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
Nn
Nn
|
134 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
135 | | n0i 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
136 | 134, 135 | sylbir 204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
137 | | pm2.53 362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
138 | 136, 137 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
139 | 138 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
140 | 133, 139 | syl6 29 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Nn
Nn |
141 | 140 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Nn
Nn |
142 | 141 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Nn
Nn |
143 | 142 | adantrr 697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Nn
Nn |
144 | 143 | 3adant1 973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nn Nn Nn
Nn |
145 | 144 | impcom 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Nn Nn Nn Nn
|
146 | 128, 145 | syld 40 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn Nn Nn Nn
1c |
147 | 146 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn Nn Nn Nn
1c |
148 | 147 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nn Nn Nn
1c Nn |
149 | 148 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn Nn Nn
1c
Nn |
150 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1c 1c |
151 | 149, 150 | syl6 29 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nn Nn Nn
1c
Nn
1c
1c |
152 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
1c
1c |
153 | 152 | anbi2d 684 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1c Nn Nn Nn
Nn Nn Nn
1c |
154 | | eqeq2 2362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
1c 1c
1c
1c |
155 | 154 | imbi2d 307 |
. . . . . . . . . . . . . . . . . . . . . . . 24
1c Nn 1c Nn 1c
1c |
156 | 153, 155 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . 23
1c Nn Nn Nn
Nn 1c Nn Nn Nn
1c
Nn
1c
1c |
157 | 151, 156 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . . . 22
1c Nn Nn Nn
Nn 1c |
158 | 157 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . 21
Nn Nn Nn
Nn
1c
1c |
159 | 158 | rexlimdv 2737 |
. . . . . . . . . . . . . . . . . . . 20
Nn Nn Nn
Nn
1c
1c |
160 | 121, 159 | syld 40 |
. . . . . . . . . . . . . . . . . . 19
Nn Nn Nn
0c
Nn 1c
1c |
161 | 160 | ex 423 |
. . . . . . . . . . . . . . . . . 18
Nn Nn Nn
0c
Nn 1c
1c |
162 | 103, 161 | mpid 37 |
. . . . . . . . . . . . . . . . 17
Nn Nn Nn
1c
|
163 | 162 | 3expa 1151 |
. . . . . . . . . . . . . . . 16
Nn Nn Nn
1c
|
164 | | eleq1 2413 |
. . . . . . . . . . . . . . . . 17
|
165 | 164 | imbi1d 308 |
. . . . . . . . . . . . . . . 16
1c
1c
|
166 | 163, 165 | syl5ibrcom 213 |
. . . . . . . . . . . . . . 15
Nn Nn Nn
1c
|
167 | 100, 166 | sylan2b 461 |
. . . . . . . . . . . . . 14
Nn Nn Nn
∼
1c
|
168 | 167 | rexlimdvva 2745 |
. . . . . . . . . . . . 13
Nn Nn Nn
∼
1c
|
169 | 97, 168 | syl5bi 208 |
. . . . . . . . . . . 12
Nn Nn Nn
1c 1c |
170 | 169 | imp3a 420 |
. . . . . . . . . . 11
Nn Nn Nn
1c
1c |
171 | 96, 170 | syl5bi 208 |
. . . . . . . . . 10
Nn Nn Nn
1c
1c |
172 | 171 | exlimdv 1636 |
. . . . . . . . 9
Nn Nn Nn
1c 1c |
173 | 95, 172 | syl5bi 208 |
. . . . . . . 8
Nn Nn Nn
1c 1c |
174 | 173 | orrd 367 |
. . . . . . 7
Nn Nn Nn
1c
1c
|
175 | 174 | exp31 587 |
. . . . . 6
Nn Nn Nn
1c
1c |
176 | 175 | com23 72 |
. . . . 5
Nn Nn
Nn 1c 1c |
177 | 176 | ralrimdv 2703 |
. . . 4
Nn Nn
Nn 1c 1c |
178 | 44, 59, 70, 75, 80, 94, 177 | finds 4411 |
. . 3
Nn Nn
|
179 | | ineq2 3451 |
. . . . . 6
|
180 | 179 | eqeq1d 2361 |
. . . . 5
|
181 | | eqeq2 2362 |
. . . . 5
|
182 | 180, 181 | orbi12d 690 |
. . . 4
|
183 | 182 | rspccv 2952 |
. . 3
Nn
Nn
|
184 | 178, 183 | syl 15 |
. 2
Nn Nn |
185 | 184 | imp 418 |
1
Nn Nn
|