Step | Hyp | Ref
| Expression |
1 | | sseq1 3292 |
. . . . 5
|
2 | | eleq1 2413 |
. . . . 5
Fin
Fin |
3 | 1, 2 | imbi12d 311 |
. . . 4
Fin Fin |
4 | 3 | imbi2d 307 |
. . 3
Fin Fin Fin
Fin |
5 | | sseq2 3293 |
. . . . 5
|
6 | 5 | imbi1d 308 |
. . . 4
Fin Fin |
7 | | elfin 4420 |
. . . . 5
Fin Nn |
8 | | vex 2862 |
. . . . . . . . . . . . 13
|
9 | 8 | elcompl 3225 |
. . . . . . . . . . . 12
∼ Sk 1
Sk k ∼ Fin k k1c Sk 1
Sk k ∼ Fin k k1c |
10 | | alcom 1737 |
. . . . . . . . . . . . 13
Fin
Fin |
11 | | impexp 433 |
. . . . . . . . . . . . . . . 16
Fin
Fin |
12 | 11 | albii 1566 |
. . . . . . . . . . . . . . 15
Fin
Fin |
13 | | 19.21v 1890 |
. . . . . . . . . . . . . . 15
Fin Fin |
14 | 12, 13 | bitri 240 |
. . . . . . . . . . . . . 14
Fin
Fin |
15 | 14 | albii 1566 |
. . . . . . . . . . . . 13
Fin Fin |
16 | 8 | elimak 4259 |
. . . . . . . . . . . . . . 15
Sk 1
Sk k ∼ Fin k k1c 1c
Sk 1
Sk k ∼ Fin k |
17 | | df-rex 2620 |
. . . . . . . . . . . . . . . 16
1c Sk 1
Sk k ∼ Fin k
1c
Sk 1
Sk k ∼ Fin k |
18 | | el1c 4139 |
. . . . . . . . . . . . . . . . . . . 20
1c
|
19 | 18 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . 19
1c Sk 1
Sk k ∼ Fin k
Sk 1
Sk k ∼ Fin k |
20 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . 19
Sk 1
Sk k ∼ Fin k
Sk 1
Sk k ∼ Fin k |
21 | 19, 20 | bitr4i 243 |
. . . . . . . . . . . . . . . . . 18
1c Sk 1
Sk k ∼ Fin k
Sk 1
Sk k ∼ Fin k |
22 | 21 | exbii 1582 |
. . . . . . . . . . . . . . . . 17
1c Sk 1
Sk k ∼ Fin k Sk 1
Sk k ∼ Fin k |
23 | | excom 1741 |
. . . . . . . . . . . . . . . . 17
Sk 1
Sk k ∼ Fin k Sk 1
Sk k ∼ Fin k |
24 | 22, 23 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
1c Sk 1
Sk k ∼ Fin k Sk 1
Sk k ∼ Fin k |
25 | | snex 4111 |
. . . . . . . . . . . . . . . . . . 19
|
26 | | opkeq1 4059 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | 26 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . 19
Sk 1
Sk k ∼ Fin k
Sk 1
Sk k ∼ Fin k |
28 | 25, 27 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . 18
Sk 1
Sk k ∼ Fin k
Sk 1
Sk k ∼ Fin k |
29 | | elin 3219 |
. . . . . . . . . . . . . . . . . 18
Sk 1
Sk k ∼ Fin k Sk 1 Sk k ∼ Fin k |
30 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30, 8 | elssetk 4270 |
. . . . . . . . . . . . . . . . . . 19
Sk |
32 | 25, 8 | opkelxpk 4248 |
. . . . . . . . . . . . . . . . . . . . 21
1 Sk k ∼ Fin k
1 Sk k ∼ Fin |
33 | 8, 32 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . 20
1 Sk k ∼ Fin k
1 Sk k ∼ Fin |
34 | | snelpw1 4146 |
. . . . . . . . . . . . . . . . . . . 20
1 Sk k ∼ Fin Sk k ∼ Fin |
35 | 30 | elimak 4259 |
. . . . . . . . . . . . . . . . . . . . 21
Sk k ∼ Fin ∼ Fin
Sk |
36 | | df-rex 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
∼ Fin Sk ∼ Fin Sk |
37 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . 24
∼
Fin Sk Sk ∼ Fin |
38 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
39 | | opkelssetkg 4268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Sk |
40 | 38, 30, 39 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Sk |
41 | 38 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
∼ Fin Fin |
42 | 40, 41 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Sk ∼
Fin Fin |
43 | 37, 42 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
∼
Fin Sk
Fin |
44 | 43 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . 22
∼ Fin Sk Fin |
45 | 36, 44 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
∼ Fin Sk Fin |
46 | | exanali 1585 |
. . . . . . . . . . . . . . . . . . . . 21
Fin
Fin |
47 | 35, 45, 46 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . 20
Sk k ∼ Fin
Fin |
48 | 33, 34, 47 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
1 Sk k ∼ Fin k
Fin |
49 | 31, 48 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
Sk 1 Sk k
∼ Fin k Fin |
50 | 28, 29, 49 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
Sk 1
Sk k ∼ Fin k Fin |
51 | 50 | exbii 1582 |
. . . . . . . . . . . . . . . 16
Sk 1
Sk k ∼ Fin k
Fin |
52 | 17, 24, 51 | 3bitri 262 |
. . . . . . . . . . . . . . 15
1c Sk 1
Sk k ∼ Fin k
Fin |
53 | | exanali 1585 |
. . . . . . . . . . . . . . 15
Fin
Fin |
54 | 16, 52, 53 | 3bitri 262 |
. . . . . . . . . . . . . 14
Sk 1
Sk k ∼ Fin k k1c Fin |
55 | 54 | con2bii 322 |
. . . . . . . . . . . . 13
Fin Sk 1
Sk k ∼ Fin k k1c |
56 | 10, 15, 55 | 3bitri 262 |
. . . . . . . . . . . 12
Fin Sk 1
Sk k ∼ Fin k k1c |
57 | 9, 56 | bitr4i 243 |
. . . . . . . . . . 11
∼ Sk 1
Sk k ∼ Fin k k1c
Fin |
58 | 57 | abbi2i 2464 |
. . . . . . . . . 10
∼ Sk 1
Sk k ∼ Fin k k1c
Fin |
59 | | ssetkex 4294 |
. . . . . . . . . . . . 13
Sk |
60 | | finex 4397 |
. . . . . . . . . . . . . . . . 17
Fin |
61 | 60 | complex 4104 |
. . . . . . . . . . . . . . . 16
∼ Fin |
62 | 59, 61 | imakex 4300 |
. . . . . . . . . . . . . . 15
Sk k ∼ Fin |
63 | 62 | pw1ex 4303 |
. . . . . . . . . . . . . 14
1 Sk k ∼ Fin |
64 | | vvex 4109 |
. . . . . . . . . . . . . 14
|
65 | 63, 64 | xpkex 4289 |
. . . . . . . . . . . . 13
1 Sk k
∼ Fin k
|
66 | 59, 65 | inex 4105 |
. . . . . . . . . . . 12
Sk 1
Sk k ∼ Fin k |
67 | | 1cex 4142 |
. . . . . . . . . . . 12
1c
|
68 | 66, 67 | imakex 4300 |
. . . . . . . . . . 11
Sk 1
Sk k ∼ Fin k k1c |
69 | 68 | complex 4104 |
. . . . . . . . . 10
∼ Sk 1
Sk k ∼ Fin k k1c |
70 | 58, 69 | eqeltrri 2424 |
. . . . . . . . 9
Fin |
71 | | eleq2 2414 |
. . . . . . . . . . . . 13
0c
0c |
72 | | df-0c 4377 |
. . . . . . . . . . . . . . 15
0c
|
73 | 72 | eleq2i 2417 |
. . . . . . . . . . . . . 14
0c
|
74 | 30 | elsnc 3756 |
. . . . . . . . . . . . . 14
|
75 | 73, 74 | bitri 240 |
. . . . . . . . . . . . 13
0c
|
76 | 71, 75 | syl6bb 252 |
. . . . . . . . . . . 12
0c
|
77 | 76 | anbi1d 685 |
. . . . . . . . . . 11
0c
|
78 | 77 | imbi1d 308 |
. . . . . . . . . 10
0c Fin
Fin |
79 | 78 | 2albidv 1627 |
. . . . . . . . 9
0c
Fin
Fin |
80 | | elequ2 1715 |
. . . . . . . . . . . . 13
|
81 | 80 | anbi1d 685 |
. . . . . . . . . . . 12
|
82 | 81 | imbi1d 308 |
. . . . . . . . . . 11
Fin Fin |
83 | 82 | 2albidv 1627 |
. . . . . . . . . 10
Fin
Fin |
84 | | eleq1 2413 |
. . . . . . . . . . . . . 14
|
85 | 84 | adantl 452 |
. . . . . . . . . . . . 13
|
86 | | sseq12 3294 |
. . . . . . . . . . . . 13
|
87 | 85, 86 | anbi12d 691 |
. . . . . . . . . . . 12
|
88 | | eleq1 2413 |
. . . . . . . . . . . . 13
Fin
Fin |
89 | 88 | adantr 451 |
. . . . . . . . . . . 12
Fin Fin |
90 | 87, 89 | imbi12d 311 |
. . . . . . . . . . 11
Fin
Fin |
91 | 90 | cbval2v 2006 |
. . . . . . . . . 10
Fin
Fin |
92 | 83, 91 | syl6bb 252 |
. . . . . . . . 9
Fin
Fin |
93 | | eleq2 2414 |
. . . . . . . . . . . 12
1c
1c |
94 | 93 | anbi1d 685 |
. . . . . . . . . . 11
1c
1c
|
95 | 94 | imbi1d 308 |
. . . . . . . . . 10
1c Fin
1c
Fin |
96 | 95 | 2albidv 1627 |
. . . . . . . . 9
1c
Fin
1c
Fin |
97 | | elequ2 1715 |
. . . . . . . . . . . 12
|
98 | 97 | anbi1d 685 |
. . . . . . . . . . 11
|
99 | 98 | imbi1d 308 |
. . . . . . . . . 10
Fin Fin |
100 | 99 | 2albidv 1627 |
. . . . . . . . 9
Fin
Fin |
101 | | sseq2 3293 |
. . . . . . . . . . . . 13
|
102 | 101 | biimpa 470 |
. . . . . . . . . . . 12
|
103 | | ss0b 3580 |
. . . . . . . . . . . 12
|
104 | 102, 103 | sylib 188 |
. . . . . . . . . . 11
|
105 | | 0fin 4423 |
. . . . . . . . . . 11
Fin |
106 | 104, 105 | syl6eqel 2441 |
. . . . . . . . . 10
Fin |
107 | 106 | gen2 1547 |
. . . . . . . . 9
Fin |
108 | | sspss 3368 |
. . . . . . . . . . . . . . 15
|
109 | | dfpss4 3888 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | orbi1i 506 |
. . . . . . . . . . . . . . 15
|
111 | 108, 110 | bitri 240 |
. . . . . . . . . . . . . 14
|
112 | | simp1 955 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn
1c
Nn |
113 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
114 | 113 | snid 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
115 | | eldif 3221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
116 | 115 | simprbi 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
117 | 114, 116 | mt2 170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
118 | 117 | a1i 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn
1c
|
119 | | undif1 3625 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
120 | | snssi 3852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
121 | | ssequn2 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
122 | 120, 121 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
123 | 122 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
124 | 123 | 3ad2ant2 977 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn
1c
|
125 | 119, 124 | syl5eq 2397 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nn
1c |
126 | | simp3r 984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nn
1c
1c |
127 | 125, 126 | eqeltrd 2427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn
1c
1c |
128 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
129 | 30, 128 | difex 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
130 | 129, 113 | nnsucelr 4428 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn
1c
|
131 | 112, 118,
127, 130 | syl12anc 1180 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nn
1c
|
132 | | inass 3465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼ ∼ |
133 | | df-dif 3215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼ |
134 | | df-dif 3215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
∼ |
135 | 134 | ineq2i 3454 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
∼ |
136 | 132, 133,
135 | 3eqtr4ri 2384 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
137 | | df-ss 3259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
138 | 137 | biimpi 186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
139 | 138 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1c
|
140 | 139 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Nn
1c
|
141 | 140 | difeq1d 3384 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn
1c
|
142 | | difsn 3845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
143 | 142 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
144 | 143 | 3ad2ant2 977 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Nn
1c
|
145 | 141, 144 | eqtrd 2385 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Nn
1c
|
146 | 136, 145 | syl5eq 2397 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Nn
1c
|
147 | | df-ss 3259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 146, 147 | sylibr 203 |
. . . . . . . . . . . . . . . . . . . . . . 23
Nn
1c |
149 | 131, 148 | jca 518 |
. . . . . . . . . . . . . . . . . . . . . 22
Nn
1c
|
150 | 149 | 3adant1r 1175 |
. . . . . . . . . . . . . . . . . . . . 21
Nn
Fin
1c
|
151 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
152 | 151 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
153 | | sseq12 3294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
154 | 152, 153 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
155 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Fin
Fin |
156 | 155 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Fin Fin |
157 | 154, 156 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Fin
Fin |
158 | 157 | spc2gv 2942 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Fin
Fin |
159 | 38, 129, 158 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . 23
Fin
Fin |
160 | 159 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . 22
Nn
Fin
Fin |
161 | 160 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . 21
Nn
Fin
1c
Fin |
162 | 150, 161 | mpd 14 |
. . . . . . . . . . . . . . . . . . . 20
Nn
Fin
1c
Fin |
163 | 162 | 3exp 1150 |
. . . . . . . . . . . . . . . . . . 19
Nn
Fin
1c Fin |
164 | 163 | exp5c 599 |
. . . . . . . . . . . . . . . . . 18
Nn
Fin
1c Fin |
165 | 164 | rexlimdv 2737 |
. . . . . . . . . . . . . . . . 17
Nn
Fin
1c Fin |
166 | 165 | com23 72 |
. . . . . . . . . . . . . . . 16
Nn
Fin
1c Fin |
167 | 166 | imp3a 420 |
. . . . . . . . . . . . . . 15
Nn
Fin
1c Fin |
168 | | peano2 4403 |
. . . . . . . . . . . . . . . . . 18
Nn
1c
Nn |
169 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . 21
1c
1c |
170 | 169 | rspcev 2955 |
. . . . . . . . . . . . . . . . . . . 20
1c
Nn
1c
Nn |
171 | | elfin 4420 |
. . . . . . . . . . . . . . . . . . . 20
Fin Nn |
172 | 170, 171 | sylibr 203 |
. . . . . . . . . . . . . . . . . . 19
1c
Nn
1c Fin |
173 | 172 | ex 423 |
. . . . . . . . . . . . . . . . . 18
1c
Nn
1c
Fin |
174 | 168, 173 | syl 15 |
. . . . . . . . . . . . . . . . 17
Nn
1c
Fin |
175 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . 18
Fin
Fin |
176 | 175 | biimprd 214 |
. . . . . . . . . . . . . . . . 17
Fin Fin |
177 | 174, 176 | syl9 66 |
. . . . . . . . . . . . . . . 16
Nn
1c
Fin |
178 | 177 | adantr 451 |
. . . . . . . . . . . . . . 15
Nn
Fin 1c Fin |
179 | 167, 178 | jaod 369 |
. . . . . . . . . . . . . 14
Nn
Fin
1c
Fin |
180 | 111, 179 | syl5bi 208 |
. . . . . . . . . . . . 13
Nn
Fin
1c
Fin |
181 | 180 | com23 72 |
. . . . . . . . . . . 12
Nn
Fin
1c
Fin |
182 | 181 | imp3a 420 |
. . . . . . . . . . 11
Nn
Fin 1c
Fin |
183 | 182 | alrimivv 1632 |
. . . . . . . . . 10
Nn
Fin
1c
Fin |
184 | 183 | ex 423 |
. . . . . . . . 9
Nn
Fin
1c
Fin |
185 | 70, 79, 92, 96, 100, 107, 184 | finds 4411 |
. . . . . . . 8
Nn
Fin |
186 | 185 | 19.21bbi 1865 |
. . . . . . 7
Nn
Fin |
187 | 186 | exp3a 425 |
. . . . . 6
Nn Fin |
188 | 187 | rexlimiv 2732 |
. . . . 5
Nn
Fin |
189 | 7, 188 | sylbi 187 |
. . . 4
Fin
Fin |
190 | 6, 189 | vtoclga 2920 |
. . 3
Fin
Fin |
191 | 4, 190 | vtoclg 2914 |
. 2
Fin Fin |
192 | 191 | 3imp 1145 |
1
Fin
Fin |