Step Hyp Ref
Expression 1 cantnfs.a . . . 4
2 cantnflt.c . . . 4
3 cantnflt.a . . . 4
4 oen0 7254 . . . 4
5 1 , 2 , 3 , 4 syl21anc 1227 . . 3
6 fveq2 5871 . . . . 5
7 0ex 4582 . . . . . 6
8 cantnfval.h . . . . . . 7
9 8 seqom0g 7140 . . . . . 6
10 7 , 9 ax-mp 5 . . . . 5
11 6 , 10 syl6eq 2514 . . . 4
12 11 eleq1d 2526 . . 3
13 5 , 12 syl5ibrcom 222 . 2
14 2 adantr 465 . . . . . . 7
15 eloni 4893 . . . . . . 7
16 14 , 15 syl 16 . . . . . 6
17 cantnflt.s . . . . . . . 8
18 17 adantr 465 . . . . . . 7
19 cantnfcl.g . . . . . . . . . 10
20 19 oif 7976 . . . . . . . . 9
21 ffn 5736 . . . . . . . . 9
22 20 , 21 mp1i 12 . . . . . . . 8
23 cantnflt.k . . . . . . . . . 10
24 19 oicl 7975 . . . . . . . . . . . . 13
25 ordsuc 6649 . . . . . . . . . . . . 13
26 24 , 25 mpbi 208 . . . . . . . . . . . 12
27 ordelon 4907 . . . . . . . . . . . 12
28 26 , 23 , 27 sylancr 663 . . . . . . . . . . 11
29 ordsssuc 4969 . . . . . . . . . . 11
30 28 , 24 , 29 sylancl 662 . . . . . . . . . 10
31 23 , 30 mpbird 232 . . . . . . . . 9
32 31 adantr 465 . . . . . . . 8
33 vex 3112 . . . . . . . . . 10
34 33 sucid 4962 . . . . . . . . 9
35 simprr 757 . . . . . . . . 9
36 34 , 35 syl5eleqr 2552 . . . . . . . 8
37 fnfvima 6150 . . . . . . . 8
38 22 , 32 , 36 , 37 syl3anc 1228 . . . . . . 7
39 18 , 38 sseldd 3504 . . . . . 6
40 ordsucss 6653 . . . . . 6
41 16 , 39 , 40 sylc 60 . . . . 5
42 suppssdm 6931 . . . . . . . . . . 11
43 cantnfcl.f . . . . . . . . . . . . . 14
44 cantnfs.s . . . . . . . . . . . . . . 15
45 cantnfs.b . . . . . . . . . . . . . . 15
46 44 , 1 , 45 cantnfs 8106 . . . . . . . . . . . . . 14
47 43 , 46 mpbid 210 . . . . . . . . . . . . 13
48 47 simpld 459 . . . . . . . . . . . 12
49 fdm 5740 . . . . . . . . . . . 12
50 48 , 49 syl 16 . . . . . . . . . . 11
51 42 , 50 syl5sseq 3551 . . . . . . . . . 10
52 onss 6626 . . . . . . . . . . 11
53 45 , 52 syl 16 . . . . . . . . . 10
54 51 , 53 sstrd 3513 . . . . . . . . 9
55 54 adantr 465 . . . . . . . 8
56 23 adantr 465 . . . . . . . . . . 11
57 35 , 56 eqeltrrd 2546 . . . . . . . . . 10
58 ordsucelsuc 6657 . . . . . . . . . . 11
59 24 , 58 ax-mp 5 . . . . . . . . . 10
60 57 , 59 sylibr 212 . . . . . . . . 9
61 20 ffvelrni 6030 . . . . . . . . 9
62 60 , 61 syl 16 . . . . . . . 8
63 55 , 62 sseldd 3504 . . . . . . 7
64 suceloni 6648 . . . . . . 7
65 63 , 64 syl 16 . . . . . 6
66 1 adantr 465 . . . . . 6
67 3 adantr 465 . . . . . 6
68 oewordi 7259 . . . . . 6
69 65 , 14 , 66 , 67 , 68 syl31anc 1231 . . . . 5
70 41 , 69 mpd 15 . . . 4
71 35 fveq2d 5875 . . . . 5
72 simprl 756 . . . . . 6
73 simpl 457 . . . . . 6
74 eleq1 2529 . . . . . . . 8
75 suceq 4948 . . . . . . . . . 10
76 75 fveq2d 5875 . . . . . . . . 9
77 fveq2 5871 . . . . . . . . . . 11
78 suceq 4948 . . . . . . . . . . 11
79 77 , 78 syl 16 . . . . . . . . . 10
80 79 oveq2d 6312 . . . . . . . . 9
81 76 , 80 eleq12d 2539 . . . . . . . 8
82 74 , 81 imbi12d 320 . . . . . . 7
83 eleq1 2529 . . . . . . . 8
84 suceq 4948 . . . . . . . . . 10
85 84 fveq2d 5875 . . . . . . . . 9
86 fveq2 5871 . . . . . . . . . . 11
87 suceq 4948 . . . . . . . . . . 11
88 86 , 87 syl 16 . . . . . . . . . 10
89 88 oveq2d 6312 . . . . . . . . 9
90 85 , 89 eleq12d 2539 . . . . . . . 8
91 83 , 90 imbi12d 320 . . . . . . 7
92 eleq1 2529 . . . . . . . 8
93 suceq 4948 . . . . . . . . . 10
94 93 fveq2d 5875 . . . . . . . . 9
95 fveq2 5871 . . . . . . . . . . 11
96 suceq 4948 . . . . . . . . . . 11
97 95 , 96 syl 16 . . . . . . . . . 10
98 97 oveq2d 6312 . . . . . . . . 9
99 94 , 98 eleq12d 2539 . . . . . . . 8
100 92 , 99 imbi12d 320 . . . . . . 7
101 48 adantr 465 . . . . . . . . . . 11
102 20 ffvelrni 6030 . . . . . . . . . . . 12
103 51 sselda 3503 . . . . . . . . . . . 12
104 102 , 103 sylan2 474 . . . . . . . . . . 11
105 101 , 104 ffvelrnd 6032 . . . . . . . . . 10
106 1 adantr 465 . . . . . . . . . . . 12
107 onelon 4908 . . . . . . . . . . . 12
108 106 , 105 ,
107 syl2anc 661 . . . . . . . . . . 11
109 54 sselda 3503 . . . . . . . . . . . . 13
110 102 , 109 sylan2 474 . . . . . . . . . . . 12
111 oecl 7206 . . . . . . . . . . . 12
112 106 , 110 ,
111 syl2anc 661 . . . . . . . . . . 11
113 3 adantr 465 . . . . . . . . . . . 12
114 oen0 7254 . . . . . . . . . . . 12
115 106 , 110 ,
113 , 114 syl21anc 1227 . . . . . . . . . . 11
116 omord2 7235 . . . . . . . . . . 11
117 108 , 106 ,
112 , 115 , 116 syl31anc 1231 . . . . . . . . . 10
118 105 , 117 mpbid 210 . . . . . . . . 9
119 peano1 6719 . . . . . . . . . . . 12
120 119 a1i 11 . . . . . . . . . . 11
121 44 , 1 , 45 , 19 , 43 , 8 cantnfsuc 8110 . . . . . . . . . . 11
122 120 , 121 sylan2 474 . . . . . . . . . 10
123 10 oveq2i 6307 . . . . . . . . . . 11
124 omcl 7205 . . . . . . . . . . . . 13
125 112 , 108 ,
124 syl2anc 661 . . . . . . . . . . . 12
126 oa0 7185 . . . . . . . . . . . 12
127 125 , 126 syl 16 . . . . . . . . . . 11
128 123 , 127 syl5eq 2510 . . . . . . . . . 10
129 122 , 128 eqtrd 2498 . . . . . . . . 9
130 oesuc 7196 . . . . . . . . . 10
131 106 , 110 ,
130 syl2anc 661 . . . . . . . . 9
132 118 , 129 ,
131 3eltr4d 2560 . . . . . . . 8
133 132 ex 434 . . . . . . 7
134 ordtr 4897 . . . . . . . . . . . 12
135 24 , 134 ax-mp 5 . . . . . . . . . . 11
136 trsuc 4967 . . . . . . . . . . 11
137 135 , 136 mpan 670 . . . . . . . . . 10
138 137 imim1i 58 . . . . . . . . 9
139 1 ad2antrr 725 . . . . . . . . . . . . . . . 16
140 eloni 4893 . . . . . . . . . . . . . . . 16
141 139 , 140 syl 16 . . . . . . . . . . . . . . 15
142 48 ad2antrr 725 . . . . . . . . . . . . . . . 16
143 51 ad2antrr 725 . . . . . . . . . . . . . . . . 17
144 20 ffvelrni 6030 . . . . . . . . . . . . . . . . . 18
145 144 ad2antrl 727 . . . . . . . . . . . . . . . . 17
146 143 , 145 sseldd 3504 . . . . . . . . . . . . . . . 16
147 142 , 146 ffvelrnd 6032 . . . . . . . . . . . . . . 15
148 ordsucss 6653 . . . . . . . . . . . . . . 15
149 141 , 147 ,
148 sylc 60 . . . . . . . . . . . . . 14
150 onelon 4908 . . . . . . . . . . . . . . . . 17
151 139 , 147 ,
150 syl2anc 661 . . . . . . . . . . . . . . . 16
152 suceloni 6648 . . . . . . . . . . . . . . . 16
153 151 , 152 syl 16 . . . . . . . . . . . . . . 15
154 54 ad2antrr 725 . . . . . . . . . . . . . . . . 17
155 154 , 145 sseldd 3504 . . . . . . . . . . . . . . . 16
156 oecl 7206 . . . . . . . . . . . . . . . 16
157 139 , 155 ,
156 syl2anc 661 . . . . . . . . . . . . . . 15
158 omwordi 7239 . . . . . . . . . . . . . . 15
159 153 , 139 ,
157 , 158 syl3anc 1228 . . . . . . . . . . . . . 14
160 149 , 159 mpd 15 . . . . . . . . . . . . 13
161 oesuc 7196 . . . . . . . . . . . . . 14
162 139 , 155 ,
161 syl2anc 661 . . . . . . . . . . . . 13
163 160 , 162 sseqtr4d 3540 . . . . . . . . . . . 12
164 eloni 4893 . . . . . . . . . . . . . . . . . 18
165 155 , 164 syl 16 . . . . . . . . . . . . . . . . 17
166 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
167 166 sucid 4962 . . . . . . . . . . . . . . . . . . . 20
168 166 sucex 6646 . . . . . . . . . . . . . . . . . . . . 21
169 168 epelc 4798 . . . . . . . . . . . . . . . . . . . 20
170 167 , 169 mpbir 209 . . . . . . . . . . . . . . . . . . 19
171 45 , 51 ssexd 4599 . . . . . . . . . . . . . . . . . . . . . 22
172 44 , 1 , 45 , 19 , 43 cantnfcl 8107 . . . . . . . . . . . . . . . . . . . . . . 23
173 172 simpld 459 . . . . . . . . . . . . . . . . . . . . . 22
174 19 oiiso 7983 . . . . . . . . . . . . . . . . . . . . . 22
175 171 , 173 ,
174 syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
176 175 ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
177 137 ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20
178 simprl 756 . . . . . . . . . . . . . . . . . . . 20
179 isorel 6222 . . . . . . . . . . . . . . . . . . . 20
180 176 , 177 ,
178 , 179 syl12anc 1226 . . . . . . . . . . . . . . . . . . 19
181 170 , 180 mpbii 211 . . . . . . . . . . . . . . . . . 18
182 fvex 5881 . . . . . . . . . . . . . . . . . . 19
183 182 epelc 4798 . . . . . . . . . . . . . . . . . 18
184 181 , 183 sylib 196 . . . . . . . . . . . . . . . . 17
185 ordsucss 6653 . . . . . . . . . . . . . . . . 17
186 165 , 184 ,
185 sylc 60 . . . . . . . . . . . . . . . 16
187 20 ffvelrni 6030 . . . . . . . . . . . . . . . . . . . 20
188 177 , 187 syl 16 . . . . . . . . . . . . . . . . . . 19
189 154 , 188 sseldd 3504 . . . . . . . . . . . . . . . . . 18
190 suceloni 6648 . . . . . . . . . . . . . . . . . 18
191 189 , 190 syl 16 . . . . . . . . . . . . . . . . 17
192 3 ad2antrr 725 . . . . . . . . . . . . . . . . 17
193 oewordi 7259 . . . . . . . . . . . . . . . . 17
194 191 , 155 ,
139 , 192 , 193 syl31anc 1231 . . . . . . . . . . . . . . . 16
195 186 , 194 mpd 15 . . . . . . . . . . . . . . 15
196 simprr 757 . . . . . . . . . . . . . . 15
197 195 , 196 sseldd 3504 . . . . . . . . . . . . . 14
198 peano2 6720 . . . . . . . . . . . . . . . . 17
199 198 ad2antlr 726 . . . . . . . . . . . . . . . 16
200 8 cantnfvalf 8105 . . . . . . . . . . . . . . . . 17
201 200 ffvelrni 6030 . . . . . . . . . . . . . . . 16
202 199 , 201 syl 16 . . . . . . . . . . . . . . 15
203 omcl 7205 . . . . . . . . . . . . . . . 16
204 157 , 151 ,
203 syl2anc 661 . . . . . . . . . . . . . . 15
205 oaord 7215 . . . . . . . . . . . . . . 15
206 202 , 157 ,
204 , 205 syl3anc 1228 . . . . . . . . . . . . . 14
