Step | Hyp | Ref
| Expression |
1 | | rabid 3116 |
. . . . . . 7
|
2 | | selpw 4165 |
. . . . . . . . 9
|
3 | | limord 5784 |
. . . . . . . . . . . . . . . . . . . 20
|
4 | | ordsson 6989 |
. . . . . . . . . . . . . . . . . . . 20
|
5 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . . . 21
|
6 | 5 | expcom 451 |
. . . . . . . . . . . . . . . . . . . 20
|
7 | 3, 4, 6 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
8 | 7 | imp 445 |
. . . . . . . . . . . . . . . . . 18
|
9 | 8 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
10 | | ssel2 3598 |
. . . . . . . . . . . . . . . . . . 19
|
11 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . 19
|
12 | | ordirr 5741 |
. . . . . . . . . . . . . . . . . . 19
|
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
14 | | ssel 3597 |
. . . . . . . . . . . . . . . . . . . 20
|
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
|
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
17 | 13, 16 | mtod 189 |
. . . . . . . . . . . . . . . . 17
|
18 | 9, 17 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
19 | | simpl2 1065 |
. . . . . . . . . . . . . . . . 17
|
20 | | sstr 3611 |
. . . . . . . . . . . . . . . . 17
|
21 | 19, 20 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
22 | 18, 21 | mtand 691 |
. . . . . . . . . . . . . . 15
|
23 | | simpl3 1066 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | sseq1d 3632 |
. . . . . . . . . . . . . . 15
|
25 | 22, 24 | mtbird 315 |
. . . . . . . . . . . . . 14
|
26 | | unissb 4469 |
. . . . . . . . . . . . . 14
|
27 | 25, 26 | sylnib 318 |
. . . . . . . . . . . . 13
|
28 | 27 | nrexdv 3001 |
. . . . . . . . . . . 12
|
29 | | ssel 3597 |
. . . . . . . . . . . . . . . . 17
|
30 | | ssel 3597 |
. . . . . . . . . . . . . . . . 17
|
31 | | ontri1 5757 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | 31 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
|
33 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 33, 34 | brcnv 5305 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | | epel 5032 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | 35, 36 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 37 | notbii 310 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 32, 38 | syl6bbr 278 |
. . . . . . . . . . . . . . . . . 18
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
41 | 29, 30, 40 | syl2and 500 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | impl 650 |
. . . . . . . . . . . . . . 15
|
43 | 42 | ralbidva 2985 |
. . . . . . . . . . . . . 14
|
44 | 43 | rexbidva 3049 |
. . . . . . . . . . . . 13
|
45 | 9, 44 | syl 17 |
. . . . . . . . . . . 12
|
46 | 28, 45 | mtbid 314 |
. . . . . . . . . . 11
|
47 | | vex 3203 |
. . . . . . . . . . . . 13
|
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
|
49 | | epweon 6983 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | wess 5101 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
|
52 | | weso 5105 |
. . . . . . . . . . . . . . . . . 18
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
54 | | cnvso 5674 |
. . . . . . . . . . . . . . . . 17
|
55 | 53, 54 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . 15
|
57 | | onssnum 8863 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 47, 57 | mpan 706 |
. . . . . . . . . . . . . . . . . 18
|
59 | | cardid2 8779 |
. . . . . . . . . . . . . . . . . 18
|
60 | | ensym 8005 |
. . . . . . . . . . . . . . . . . 18
|
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
62 | | nnsdom 8551 |
. . . . . . . . . . . . . . . . 17
|
63 | | ensdomtr 8096 |
. . . . . . . . . . . . . . . . 17
|
64 | 61, 62, 63 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
65 | | isfinite 8549 |
. . . . . . . . . . . . . . . 16
|
66 | 64, 65 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
67 | | wofi 8209 |
. . . . . . . . . . . . . . 15
|
68 | 56, 66, 67 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
69 | 9, 68 | sylan 488 |
. . . . . . . . . . . . 13
|
70 | | wefr 5104 |
. . . . . . . . . . . . 13
|
71 | 69, 70 | syl 17 |
. . . . . . . . . . . 12
|
72 | | ssid 3624 |
. . . . . . . . . . . . 13
|
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
|
74 | | unieq 4444 |
. . . . . . . . . . . . . . . . . . 19
|
75 | | uni0 4465 |
. . . . . . . . . . . . . . . . . . 19
|
76 | 74, 75 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
|
77 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
|
78 | 76, 77 | syl5ib 234 |
. . . . . . . . . . . . . . . . 17
|
79 | | nlim0 5783 |
. . . . . . . . . . . . . . . . . 18
|
80 | | limeq 5735 |
. . . . . . . . . . . . . . . . . 18
|
81 | 79, 80 | mtbiri 317 |
. . . . . . . . . . . . . . . . 17
|
82 | 78, 81 | syl6 35 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | necon2ad 2809 |
. . . . . . . . . . . . . . 15
|
84 | 83 | impcom 446 |
. . . . . . . . . . . . . 14
|
85 | 84 | 3adant2 1080 |
. . . . . . . . . . . . 13
|
86 | 85 | adantr 481 |
. . . . . . . . . . . 12
|
87 | | fri 5076 |
. . . . . . . . . . . 12
|
88 | 48, 71, 73, 86, 87 | syl22anc 1327 |
. . . . . . . . . . 11
|
89 | 46, 88 | mtand 691 |
. . . . . . . . . 10
|
90 | | cardon 8770 |
. . . . . . . . . . 11
|
91 | | eloni 5733 |
. . . . . . . . . . 11
|
92 | | ordom 7074 |
. . . . . . . . . . . 12
|
93 | | ordtri1 5756 |
. . . . . . . . . . . 12
|
94 | 92, 93 | mpan 706 |
. . . . . . . . . . 11
|
95 | 90, 91, 94 | mp2b 10 |
. . . . . . . . . 10
|
96 | 89, 95 | sylibr 224 |
. . . . . . . . 9
|
97 | 2, 96 | syl3an2b 1363 |
. . . . . . . 8
|
98 | 97 | 3expb 1266 |
. . . . . . 7
|
99 | 1, 98 | sylan2b 492 |
. . . . . 6
|
100 | 99 | ralrimiva 2966 |
. . . . 5
|
101 | | ssiin 4570 |
. . . . 5
|
102 | 100, 101 | sylibr 224 |
. . . 4
|
103 | | cflim2.1 |
. . . . 5
|
104 | 103 | cflim3 9084 |
. . . 4
|
105 | 102, 104 | sseqtr4d 3642 |
. . 3
|
106 | | fvex 6201 |
. . . . . . 7
|
107 | 106 | dfiin2 4555 |
. . . . . 6
|
108 | 104, 107 | syl6eq 2672 |
. . . . 5
|
109 | | cardlim 8798 |
. . . . . . . . 9
|
110 | | sseq2 3627 |
. . . . . . . . . 10
|
111 | | limeq 5735 |
. . . . . . . . . 10
|
112 | 110, 111 | bibi12d 335 |
. . . . . . . . 9
|
113 | 109, 112 | mpbiri 248 |
. . . . . . . 8
|
114 | 113 | rexlimivw 3029 |
. . . . . . 7
|
115 | 114 | ss2abi 3674 |
. . . . . 6
|
116 | | eleq1 2689 |
. . . . . . . . . 10
|
117 | 90, 116 | mpbiri 248 |
. . . . . . . . 9
|
118 | 117 | rexlimivw 3029 |
. . . . . . . 8
|
119 | 118 | abssi 3677 |
. . . . . . 7
|
120 | | fvex 6201 |
. . . . . . . . 9
|
121 | 108, 120 | syl6eqelr 2710 |
. . . . . . . 8
|
122 | | intex 4820 |
. . . . . . . 8
|
123 | 121, 122 | sylibr 224 |
. . . . . . 7
|
124 | | onint 6995 |
. . . . . . 7
|
125 | 119, 123,
124 | sylancr 695 |
. . . . . 6
|
126 | 115, 125 | sseldi 3601 |
. . . . 5
|
127 | 108, 126 | eqeltrd 2701 |
. . . 4
|
128 | | sseq2 3627 |
. . . . . 6
|
129 | | limeq 5735 |
. . . . . 6
|
130 | 128, 129 | bibi12d 335 |
. . . . 5
|
131 | 120, 130 | elab 3350 |
. . . 4
|
132 | 127, 131 | sylib 208 |
. . 3
|
133 | 105, 132 | mpbid 222 |
. 2
|
134 | | eloni 5733 |
. . . . . . 7
|
135 | | ordzsl 7045 |
. . . . . . 7
|
136 | 134, 135 | sylib 208 |
. . . . . 6
|
137 | | df-3or 1038 |
. . . . . . 7
|
138 | | orcom 402 |
. . . . . . 7
|
139 | | df-or 385 |
. . . . . . 7
|
140 | 137, 138,
139 | 3bitri 286 |
. . . . . 6
|
141 | 136, 140 | sylib 208 |
. . . . 5
|
142 | | fveq2 6191 |
. . . . . . . . 9
|
143 | | cf0 9073 |
. . . . . . . . 9
|
144 | 142, 143 | syl6eq 2672 |
. . . . . . . 8
|
145 | | limeq 5735 |
. . . . . . . 8
|
146 | 144, 145 | syl 17 |
. . . . . . 7
|
147 | 79, 146 | mtbiri 317 |
. . . . . 6
|
148 | | 1n0 7575 |
. . . . . . . . . 10
|
149 | | df1o2 7572 |
. . . . . . . . . . . 12
|
150 | 149 | unieqi 4445 |
. . . . . . . . . . 11
|
151 | | 0ex 4790 |
. . . . . . . . . . . 12
|
152 | 151 | unisn 4451 |
. . . . . . . . . . 11
|
153 | 150, 152 | eqtri 2644 |
. . . . . . . . . 10
|
154 | 148, 153 | neeqtrri 2867 |
. . . . . . . . 9
|
155 | | limuni 5785 |
. . . . . . . . . 10
|
156 | 155 | necon3ai 2819 |
. . . . . . . . 9
|
157 | 154, 156 | ax-mp 5 |
. . . . . . . 8
|
158 | | fveq2 6191 |
. . . . . . . . . 10
|
159 | | cfsuc 9079 |
. . . . . . . . . 10
|
160 | 158, 159 | sylan9eqr 2678 |
. . . . . . . . 9
|
161 | | limeq 5735 |
. . . . . . . . 9
|
162 | 160, 161 | syl 17 |
. . . . . . . 8
|
163 | 157, 162 | mtbiri 317 |
. . . . . . 7
|
164 | 163 | rexlimiva 3028 |
. . . . . 6
|
165 | 147, 164 | jaoi 394 |
. . . . 5
|
166 | 141, 165 | syl6 35 |
. . . 4
|
167 | 166 | con4d 114 |
. . 3
|
168 | | cff 9070 |
. . . . . . . . 9
|
169 | 168 | fdmi 6052 |
. . . . . . . 8
|
170 | 169 | eleq2i 2693 |
. . . . . . 7
|
171 | | ndmfv 6218 |
. . . . . . 7
|
172 | 170, 171 | sylnbir 321 |
. . . . . 6
|
173 | 172, 145 | syl 17 |
. . . . 5
|
174 | 79, 173 | mtbiri 317 |
. . . 4
|
175 | 174 | pm2.21d 118 |
. . 3
|
176 | 167, 175 | pm2.61i 176 |
. 2
|
177 | 133, 176 | impbii 199 |
1
|