Step | Hyp | Ref
| Expression |
1 | | cantnfs.a |
. . . 4
   |
2 | | cantnflt.c |
. . . 4
   |
3 | | cantnflt.a |
. . . 4

  |
4 | | oen0 7138 |
. . . 4
         |
5 | 1, 2, 3, 4 | syl21anc 1218 |
. . 3

    |
6 | | fveq2 5802 |
. . . . 5

          |
7 | | 0ex 4533 |
. . . . . 6
 |
8 | | cantnfval.h |
. . . . . . 7
seq𝜔  
                      |
9 | 8 | seqom0g 7024 |
. . . . . 6

      |
10 | 7, 9 | ax-mp 5 |
. . . . 5
     |
11 | 6, 10 | syl6eq 2511 |
. . . 4

      |
12 | 11 | eleq1d 2523 |
. . 3

      
     |
13 | 5, 12 | syl5ibrcom 222 |
. 2
           |
14 | 2 | adantr 465 |
. . . . . . 7
 
     |
15 | | eloni 4840 |
. . . . . . 7
   |
16 | 14, 15 | syl 16 |
. . . . . 6
 
  
  |
17 | | cantnflt.s |
. . . . . . . 8
    
  |
18 | 17 | adantr 465 |
. . . . . . 7
 
         |
19 | | cantnfcl.g |
. . . . . . . . . 10
OrdIso  supp    |
20 | 19 | oif 7858 |
. . . . . . . . 9
     supp   |
21 | | ffn 5670 |
. . . . . . . . 9
      supp 
  |
22 | 20, 21 | mp1i 12 |
. . . . . . . 8
 
     |
23 | | cantnflt.k |
. . . . . . . . . 10
   |
24 | 19 | oicl 7857 |
. . . . . . . . . . . . 13
 |
25 | | ordsuc 6538 |
. . . . . . . . . . . . 13

  |
26 | 24, 25 | mpbi 208 |
. . . . . . . . . . . 12
 |
27 | | ordelon 4854 |
. . . . . . . . . . . 12
 

  |
28 | 26, 23, 27 | sylancr 663 |
. . . . . . . . . . 11
   |
29 | | ordsssuc 4916 |
. . . . . . . . . . 11
       |
30 | 28, 24, 29 | sylancl 662 |
. . . . . . . . . 10
     |
31 | 23, 30 | mpbird 232 |
. . . . . . . . 9

  |
32 | 31 | adantr 465 |
. . . . . . . 8
 
     |
33 | | vex 3081 |
. . . . . . . . . 10
 |
34 | 33 | sucid 4909 |
. . . . . . . . 9
 |
35 | | simprr 756 |
. . . . . . . . 9
 
     |
36 | 34, 35 | syl5eleqr 2549 |
. . . . . . . 8
 
     |
37 | | fnfvima 6067 |
. . . . . . . 8
 

          |
38 | 22, 32, 36, 37 | syl3anc 1219 |
. . . . . . 7
 
             |
39 | 18, 38 | sseldd 3468 |
. . . . . 6
 
         |
40 | | ordsucss 6542 |
. . . . . 6

    
       |
41 | 16, 39, 40 | sylc 60 |
. . . . 5
 
  
      |
42 | | suppssdm 6816 |
. . . . . . . . . . 11
 supp 
 |
43 | | cantnfcl.f |
. . . . . . . . . . . . . 14
   |
44 | | cantnfs.s |
. . . . . . . . . . . . . . 15
 CNF   |
45 | | cantnfs.b |
. . . . . . . . . . . . . . 15
   |
46 | 44, 1, 45 | cantnfs 7988 |
. . . . . . . . . . . . . 14
       finSupp     |
47 | 43, 46 | mpbid 210 |
. . . . . . . . . . . . 13
      finSupp
   |
48 | 47 | simpld 459 |
. . . . . . . . . . . 12
       |
49 | | fdm 5674 |
. . . . . . . . . . . 12
       |
50 | 48, 49 | syl 16 |
. . . . . . . . . . 11
   |
51 | 42, 50 | syl5sseq 3515 |
. . . . . . . . . 10
  supp    |
52 | | onss 6515 |
. . . . . . . . . . 11
   |
53 | 45, 52 | syl 16 |
. . . . . . . . . 10

  |
54 | 51, 53 | sstrd 3477 |
. . . . . . . . 9
  supp    |
55 | 54 | adantr 465 |
. . . . . . . 8
 
    supp    |
56 | 23 | adantr 465 |
. . . . . . . . . . 11
 
     |
57 | 35, 56 | eqeltrrd 2543 |
. . . . . . . . . 10
 
  
  |
58 | | ordsucelsuc 6546 |
. . . . . . . . . . 11


   |
59 | 24, 58 | ax-mp 5 |
. . . . . . . . . 10

  |
60 | 57, 59 | sylibr 212 |
. . . . . . . . 9
 
     |
61 | 20 | ffvelrni 5954 |
. . . . . . . . 9
      supp    |
62 | 60, 61 | syl 16 |
. . . . . . . 8
 
        supp    |
63 | 55, 62 | sseldd 3468 |
. . . . . . 7
 
         |
64 | | suceloni 6537 |
. . . . . . 7
           |
65 | 63, 64 | syl 16 |
. . . . . 6
 
  
      |
66 | 1 | adantr 465 |
. . . . . 6
 
     |
67 | 3 | adantr 465 |
. . . . . 6
 
     |
68 | | oewordi 7143 |
. . . . . 6
        
                |
69 | 65, 14, 66, 67, 68 | syl31anc 1222 |
. . . . 5
 
       
      
    |
70 | 41, 69 | mpd 15 |
. . . 4
 
             |
71 | 35 | fveq2d 5806 |
. . . . 5
 
             |
72 | | simprl 755 |
. . . . . 6
 
     |
73 | | simpl 457 |
. . . . . 6
 
     |
74 | | eleq1 2526 |
. . . . . . . 8


   |
75 | | suceq 4895 |
. . . . . . . . . 10

  |
76 | 75 | fveq2d 5806 |
. . . . . . . . 9

  
       |
77 | | fveq2 5802 |
. . . . . . . . . . 11

          |
78 | | suceq 4895 |
. . . . . . . . . . 11
        
          |
79 | 77, 78 | syl 16 |
. . . . . . . . . 10

          |
80 | 79 | oveq2d 6219 |
. . . . . . . . 9

              |
81 | 76, 80 | eleq12d 2536 |
. . . . . . . 8

                        |
82 | 74, 81 | imbi12d 320 |
. . . . . . 7

            
               |
83 | | eleq1 2526 |
. . . . . . . 8
     |
84 | | suceq 4895 |
. . . . . . . . . 10

  |
85 | 84 | fveq2d 5806 |
. . . . . . . . 9
           |
86 | | fveq2 5802 |
. . . . . . . . . . 11
           |
87 | | suceq 4895 |
. . . . . . . . . . 11
                   |
88 | 86, 87 | syl 16 |
. . . . . . . . . 10
           |
89 | 88 | oveq2d 6219 |
. . . . . . . . 9
               |
90 | 85, 89 | eleq12d 2536 |
. . . . . . . 8
                         |
91 | 83, 90 | imbi12d 320 |
. . . . . . 7
             
               |
92 | | eleq1 2526 |
. . . . . . . 8
 
   |
93 | | suceq 4895 |
. . . . . . . . . 10
   |
94 | 93 | fveq2d 5806 |
. . . . . . . . 9
           |
95 | | fveq2 5802 |
. . . . . . . . . . 11
       
   |
96 | | suceq 4895 |
. . . . . . . . . . 11
               
   |
97 | 95, 96 | syl 16 |
. . . . . . . . . 10
           |
98 | 97 | oveq2d 6219 |
. . . . . . . . 9
          
    |
99 | 94, 98 | eleq12d 2536 |
. . . . . . . 8
                         |
100 | 92, 99 | imbi12d 320 |
. . . . . . 7
  
  
       

              |
101 | 48 | adantr 465 |
. . . . . . . . . . 11
 

      |
102 | 20 | ffvelrni 5954 |
. . . . . . . . . . . 12
      supp    |
103 | 51 | sselda 3467 |
. . . . . . . . . . . 12
 
     supp         |
104 | 102, 103 | sylan2 474 |
. . . . . . . . . . 11
 

      |
105 | 101, 104 | ffvelrnd 5956 |
. . . . . . . . . 10
 

          |
106 | 1 | adantr 465 |
. . . . . . . . . . . 12
 

  |
107 | | onelon 4855 |
. . . . . . . . . . . 12
                     |
108 | 106, 105,
107 | syl2anc 661 |
. . . . . . . . . . 11
 

          |
109 | 54 | sselda 3467 |
. . . . . . . . . . . . 13
 
     supp         |
110 | 102, 109 | sylan2 474 |
. . . . . . . . . . . 12
 

      |
111 | | oecl 7090 |
. . . . . . . . . . . 12
               |
112 | 106, 110,
111 | syl2anc 661 |
. . . . . . . . . . 11
 

        |
113 | 3 | adantr 465 |
. . . . . . . . . . . 12
 

  |
114 | | oen0 7138 |
. . . . . . . . . . . 12
        
        |
115 | 106, 110,
113, 114 | syl21anc 1218 |
. . . . . . . . . . 11
 

        |
116 | | omord2 7119 |
. . . . . . . . . . 11
                                 
                           |
117 | 108, 106,
112, 115, 116 | syl31anc 1222 |
. . . . . . . . . 10
 

                                    |
118 | 105, 117 | mpbid 210 |
. . . . . . . . 9
 

                          |
119 | | peano1 6608 |
. . . . . . . . . . . 12
 |
120 | 119 | a1i 11 |
. . . . . . . . . . 11
   |
121 | 44, 1, 45, 19, 43, 8 | cantnfsuc 7992 |
. . . . . . . . . . 11
 
                             |
122 | 120, 121 | sylan2 474 |
. . . . . . . . . 10
 

                            |
123 | 10 | oveq2i 6214 |
. . . . . . . . . . 11
                                         |
124 | | omcl 7089 |
. . . . . . . . . . . . 13
                                   |
125 | 112, 108,
124 | syl2anc 661 |
. . . . . . . . . . . 12
 

                  |
126 | | oa0 7069 |
. . . . . . . . . . . 12
                                                     |
127 | 125, 126 | syl 16 |
. . . . . . . . . . 11
 

                                    |
128 | 123, 127 | syl5eq 2507 |
. . . . . . . . . 10
 

                                        |
129 | 122, 128 | eqtrd 2495 |
. . . . . . . . 9
 

                      |
130 | | oesuc 7080 |
. . . . . . . . . 10
                       |
131 | 106, 110,
130 | syl2anc 661 |
. . . . . . . . 9
 

                |
132 | 118, 129,
131 | 3eltr4d 2557 |
. . . . . . . 8
 

            |
133 | 132 | ex 434 |
. . . . . . 7
 
             |
134 | | ordtr 4844 |
. . . . . . . . . . . 12

  |
135 | 24, 134 | ax-mp 5 |
. . . . . . . . . . 11
 |
136 | | trsuc 4914 |
. . . . . . . . . . 11
 

  |
137 | 135, 136 | mpan 670 |
. . . . . . . . . 10
   |
138 | 137 | imim1i 58 |
. . . . . . . . 9
             
             |
139 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
    
           
  |
140 | | eloni 4840 |
. . . . . . . . . . . . . . . 16
   |
141 | 139, 140 | syl 16 |
. . . . . . . . . . . . . . 15
    
              |
142 | 48 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
    
                  |
143 | 51 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
    
             supp
   |
144 | 20 | ffvelrni 5954 |
. . . . . . . . . . . . . . . . . 18
      supp    |
145 | 144 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
    
                 supp    |
146 | 143, 145 | sseldd 3468 |
. . . . . . . . . . . . . . . 16
    
                  |
147 | 142, 146 | ffvelrnd 5956 |
. . . . . . . . . . . . . . 15
    
                      |
148 | | ordsucss 6542 |
. . . . . . . . . . . . . . 15

              
 
   |
149 | 141, 147,
148 | sylc 60 |
. . . . . . . . . . . . . 14
    
                   
  |
150 | | onelon 4855 |
. . . . . . . . . . . . . . . . 17
       
             |
151 | 139, 147,
150 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
    
                      |
152 | | suceloni 6537 |
. . . . . . . . . . . . . . . 16
      
            |
153 | 151, 152 | syl 16 |
. . . . . . . . . . . . . . 15
    
                      |
154 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
    
             supp
   |
155 | 154, 145 | sseldd 3468 |
. . . . . . . . . . . . . . . 16
    
                  |
156 | | oecl 7090 |
. . . . . . . . . . . . . . . 16
               |
157 | 139, 155,
156 | syl2anc 661 |
. . . . . . . . . . . . . . 15
    
                    |
158 | | omwordi 7123 |
. . . . . . . . . . . . . . 15
          
                              
           |
159 | 153, 139,
157, 158 | syl3anc 1219 |
. . . . . . . . . . . . . 14
    
            
                                   |
160 | 149, 159 | mpd 15 |
. . . . . . . . . . . . 13
    
                        
             |
161 | | oesuc 7080 |
. . . . . . . . . . . . . 14
                       |
162 | 139, 155,
161 | syl2anc 661 |
. . . . . . . . . . . . 13
    
                            |
163 | 160, 162 | sseqtr4d 3504 |
. . . . . . . . . . . 12
    
                        
      
    |
164 | | eloni 4840 |
. . . . . . . . . . . . . . . . . 18
           |
165 | 155, 164 | syl 16 |
. . . . . . . . . . . . . . . . 17
    
                  |
166 | | vex 3081 |
. . . . . . . . . . . . . . . . . . . . 21
 |
167 | 166 | sucid 4909 |
. . . . . . . . . . . . . . . . . . . 20
 |
168 | 166 | sucex 6535 |
. . . . . . . . . . . . . . . . . . . . 21
 |
169 | 168 | epelc 4745 |
. . . . . . . . . . . . . . . . . . . 20

  |
170 | 167, 169 | mpbir 209 |
. . . . . . . . . . . . . . . . . . 19
 |
171 | 45, 51 | ssexd 4550 |
. . . . . . . . . . . . . . . . . . . . . 22
  supp    |
172 | 44, 1, 45, 19, 43 | cantnfcl 7989 |
. . . . . . . . . . . . . . . . . . . . . . 23
  supp     |
173 | 172 | simpld 459 |
. . . . . . . . . . . . . . . . . . . . . 22
  supp    |
174 | 19 | oiiso 7865 |
. . . . . . . . . . . . . . . . . . . . . 22
   supp 

supp      supp
    |
175 | 171, 173,
174 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . . 21

   supp     |
176 | 175 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
    
               supp     |
177 | 137 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
    
              |
178 | | simprl 755 |
. . . . . . . . . . . . . . . . . . . 20
    
           
  |
179 | | isorel 6129 |
. . . . . . . . . . . . . . . . . . . 20
 
   supp      
           |
180 | 176, 177,
178, 179 | syl12anc 1217 |
. . . . . . . . . . . . . . . . . . 19
    
                   
    |
181 | 170, 180 | mpbii 211 |
. . . . . . . . . . . . . . . . . 18
    
                  
   |
182 | | fvex 5812 |
. . . . . . . . . . . . . . . . . . 19
  
  |
183 | 182 | epelc 4745 |
. . . . . . . . . . . . . . . . . 18
        
          |
184 | 181, 183 | sylib 196 |
. . . . . . . . . . . . . . . . 17
    
                  
   |
185 | | ordsucss 6542 |
. . . . . . . . . . . . . . . . 17
            
            |
186 | 165, 184,
185 | sylc 60 |
. . . . . . . . . . . . . . . 16
    
               
      |
187 | 20 | ffvelrni 5954 |
. . . . . . . . . . . . . . . . . . . 20
      supp    |
188 | 177, 187 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
    
                 supp    |
189 | 154, 188 | sseldd 3468 |
. . . . . . . . . . . . . . . . . 18
    
                  |
190 | | suceloni 6537 |
. . . . . . . . . . . . . . . . . 18
           |
191 | 189, 190 | syl 16 |
. . . . . . . . . . . . . . . . 17
    
                  |
192 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
    
              |
193 | | oewordi 7143 |
. . . . . . . . . . . . . . . . 17
         
  
                        |
194 | 191, 155,
139, 192, 193 | syl31anc 1222 |
. . . . . . . . . . . . . . . 16
    
            
                       |
195 | 186, 194 | mpd 15 |
. . . . . . . . . . . . . . 15
    
                 
        |
196 | | simprr 756 |
. . . . . . . . . . . . . . 15
    
                        |
197 | 195, 196 | sseldd 3468 |
. . . . . . . . . . . . . 14
    
                   
    |
198 | | peano2 6609 |
. . . . . . . . . . . . . . . . 17

  |
199 | 198 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
    
           
  |
200 | 8 | cantnfvalf 7987 |
. . . . . . . . . . . . . . . . 17
     |
201 | 200 | ffvelrni 5954 |
. . . . . . . . . . . . . . . 16
       |
202 | 199, 201 | syl 16 |
. . . . . . . . . . . . . . 15
    
                  |
203 | | omcl 7089 |
. . . . . . . . . . . . . . . 16
             
                     |
204 | 157, 151,
203 | syl2anc 661 |
. . . . . . . . . . . . . . 15
    
                              |
205 | | oaord 7099 |
. . . . . . . . . . . . . . 15
                                
            
                                           |
206 | 202, 157,
204, 205 | syl3anc 1219 |
. . . . . . . . . . . . . 14
    
                    
       
                                           |
207 | 197, 206 | mpbid 210 |
. . . . . . . . . . . . 13
    
                                                            |
208 | 44, 1, 45, 19, 43, 8 | cantnfsuc 7992 |
. . . . . . . . . . . . . . 15
 
                             |
209 | 198, 208 | sylan2 474 |
. . . . . . . . . . . . . 14
 

  
      
                  |
210 | 209 | adantr 465 |
. . . . . . . . . . . . 13
    
                                   
    |
211 | | omsuc 7079 |
. . . . . . . . . . . . . 14
             
                                             |
212 | 157, 151,
211 | syl2anc 661 |
. . . . . . . . . . . . 13
    
                        
                             |
213 | 207, 210,
212 | 3eltr4d 2557 |
. . . . . . . . . . . 12
    
                                  |
214 | 163, 213 | sseldd 3468 |
. . . . . . . . . . 11
    
                        |
215 | 214 | exp32 605 |
. . . . . . . . . 10
 


          
  
           |
216 | 215 | a2d 26 |
. . . . . . . . 9
 

 
           
              |
217 | 138, 216 | syl5 32 |
. . . . . . . 8
 

             
              |
218 | 217 | expcom 435 |
. . . . . . 7
               
               |
219 | 82, 91, 100, 133, 218 | finds2 6617 |
. . . . . 6
  
  
           |
220 | 72, 73, 60, 219 | syl3c 61 |
. . . . 5
 
               |
221 | 71, 220 | eqeltrd 2542 |
. . . 4
 
               |
222 | 70, 221 | sseldd 3468 |
. . 3
 
           |
223 | 222 | rexlimdvaa 2948 |
. 2
            |
224 | 172 | simprd 463 |
. . . . 5
   |
225 | | peano2 6609 |
. . . . 5

  |
226 | 224, 225 | syl 16 |
. . . 4

  |
227 | | elnn 6599 |
. . . 4
     |
228 | 23, 226, 227 | syl2anc 661 |
. . 3
   |
229 | | nn0suc 6613 |
. . 3
 

   |
230 | 228, 229 | syl 16 |
. 2
  
   |
231 | 13, 223, 230 | mpjaod 381 |
1
         |