Step | Hyp | Ref
| Expression |
1 | | 0lt2o 6436 |
. . . . . 6
 |
2 | 1 | a1i 9 |
. . . . 5
 

  |
3 | | 1lt2o 6437 |
. . . . . 6
 |
4 | 3 | a1i 9 |
. . . . 5
 

  |
5 | | peano2 4591 |
. . . . . . . 8

  |
6 | 5 | adantl 277 |
. . . . . . 7
 

  |
7 | | nnfi 6866 |
. . . . . . 7
   |
8 | 6, 7 | syl 14 |
. . . . . 6
 

  |
9 | | 2ssom 6519 |
. . . . . . . . 9
 |
10 | | nninfwlpoimlemg.f |
. . . . . . . . . . 11
       |
11 | 10 | ad2antrr 488 |
. . . . . . . . . 10
           |
12 | | simpr 110 |
. . . . . . . . . . 11
    
  |
13 | 6 | adantr 276 |
. . . . . . . . . . 11
    
  |
14 | | elnn 4602 |
. . . . . . . . . . 11
     |
15 | 12, 13, 14 | syl2anc 411 |
. . . . . . . . . 10
    
  |
16 | 11, 15 | ffvelcdmd 5648 |
. . . . . . . . 9
           |
17 | 9, 16 | sselid 3153 |
. . . . . . . 8
           |
18 | | peano1 4590 |
. . . . . . . . 9
 |
19 | 18 | a1i 9 |
. . . . . . . 8
       |
20 | | nndceq 6494 |
. . . . . . . 8
      
DECID       |
21 | 17, 19, 20 | syl2anc 411 |
. . . . . . 7
     DECID       |
22 | 21 | ralrimiva 2550 |
. . . . . 6
 

 DECID       |
23 | | finexdc 6896 |
. . . . . 6
   DECID     
DECID         |
24 | 8, 22, 23 | syl2anc 411 |
. . . . 5
 

DECID         |
25 | 2, 4, 24 | ifcldcd 3569 |
. . . 4
 

  
          |
26 | | nninfwlpoimlemg.g |
. . . 4
              |
27 | 25, 26 | fmptd 5666 |
. . 3
       |
28 | | 2onn 6516 |
. . . . 5
 |
29 | 28 | elexi 2749 |
. . . 4
 |
30 | | omex 4589 |
. . . 4
 |
31 | 29, 30 | elmap 6671 |
. . 3
         |
32 | 27, 31 | sylibr 134 |
. 2
     |
33 | | simpr 110 |
. . . . . . 7
    
              |
34 | 33 | iftrued 3541 |
. . . . . 6
    
                    
          |
35 | | suceq 4399 |
. . . . . . . . . . . 12

  |
36 | 35 | rexeqdv 2679 |
. . . . . . . . . . 11
                 |
37 | 36 | ifbid 3555 |
. . . . . . . . . 10
                         |
38 | | peano2 4591 |
. . . . . . . . . . 11

  |
39 | 38 | adantl 277 |
. . . . . . . . . 10
 

  |
40 | 1 | a1i 9 |
. . . . . . . . . . 11
 

  |
41 | 3 | a1i 9 |
. . . . . . . . . . 11
 

  |
42 | | peano2 4591 |
. . . . . . . . . . . . . 14
   |
43 | 39, 42 | syl 14 |
. . . . . . . . . . . . 13
 

  |
44 | | nnfi 6866 |
. . . . . . . . . . . . 13

  |
45 | 43, 44 | syl 14 |
. . . . . . . . . . . 12
 

  |
46 | 10 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
   
       |
47 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
   
   |
48 | 43 | adantr 276 |
. . . . . . . . . . . . . . . . 17
   

  |
49 | | elnn 4602 |
. . . . . . . . . . . . . . . . 17
     |
50 | 47, 48, 49 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
   
   |
51 | 46, 50 | ffvelcdmd 5648 |
. . . . . . . . . . . . . . 15
   
       |
52 | 9, 51 | sselid 3153 |
. . . . . . . . . . . . . 14
   
       |
53 | 18 | a1i 9 |
. . . . . . . . . . . . . 14
   

  |
54 | 52, 53, 20 | syl2anc 411 |
. . . . . . . . . . . . 13
   
 DECID       |
55 | 54 | ralrimiva 2550 |
. . . . . . . . . . . 12
 


DECID
      |
56 | | finexdc 6896 |
. . . . . . . . . . . 12
 
 DECID      DECID 
       |
57 | 45, 55, 56 | syl2anc 411 |
. . . . . . . . . . 11
 

DECID         |
58 | 40, 41, 57 | ifcldcd 3569 |
. . . . . . . . . 10
 

  
          |
59 | 26, 37, 39, 58 | fvmptd3 5605 |
. . . . . . . . 9
 

      
          |
60 | | df-suc 4368 |
. . . . . . . . . . . 12

    |
61 | 60 | rexeqi 2677 |
. . . . . . . . . . 11
       

          |
62 | | rexun 3315 |
. . . . . . . . . . 11
                   
        |
63 | 61, 62 | bitri 184 |
. . . . . . . . . 10
        
               |
64 | | ifbi 3554 |
. . . . . . . . . 10
         
                                  
 
     
    |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . 9
                    
 
     
   |
66 | 59, 65 | eqtrdi 2226 |
. . . . . . . 8
 

             
 
     
    |
67 | | nnfi 6866 |
. . . . . . . . . . 11
   |
68 | 39, 67 | syl 14 |
. . . . . . . . . 10
 

  |
69 | 10 | ad2antrr 488 |
. . . . . . . . . . . . . 14
           |
70 | | simpr 110 |
. . . . . . . . . . . . . . 15
    
  |
71 | 39 | adantr 276 |
. . . . . . . . . . . . . . 15
    
  |
72 | | elnn 4602 |
. . . . . . . . . . . . . . 15
     |
73 | 70, 71, 72 | syl2anc 411 |
. . . . . . . . . . . . . 14
    
  |
74 | 69, 73 | ffvelcdmd 5648 |
. . . . . . . . . . . . 13
           |
75 | 9, 74 | sselid 3153 |
. . . . . . . . . . . 12
           |
76 | 18 | a1i 9 |
. . . . . . . . . . . 12
       |
77 | 75, 76, 20 | syl2anc 411 |
. . . . . . . . . . 11
     DECID       |
78 | 77 | ralrimiva 2550 |
. . . . . . . . . 10
 

 DECID       |
79 | | finexdc 6896 |
. . . . . . . . . 10
   DECID     
DECID         |
80 | 68, 78, 79 | syl2anc 411 |
. . . . . . . . 9
 

DECID         |
81 | | ifordc 3572 |
. . . . . . . . 9
DECID                          
  
           
          |
82 | 80, 81 | syl 14 |
. . . . . . . 8
 

          
                                  |
83 | 66, 82 | eqtrd 2210 |
. . . . . . 7
 

                             |
84 | 83 | adantr 276 |
. . . . . 6
    
                                   |
85 | | suceq 4399 |
. . . . . . . . . . 11

  |
86 | 85 | rexeqdv 2679 |
. . . . . . . . . 10
  
     
        |
87 | 86 | ifbid 3555 |
. . . . . . . . 9
                         |
88 | | simpr 110 |
. . . . . . . . 9
 

  |
89 | 40, 41, 80 | ifcldcd 3569 |
. . . . . . . . 9
 

  
          |
90 | 26, 87, 88, 89 | fvmptd3 5605 |
. . . . . . . 8
 

                 |
91 | 90 | adantr 276 |
. . . . . . 7
    
                       |
92 | 33 | iftrued 3541 |
. . . . . . 7
    
                   |
93 | 91, 92 | eqtrd 2210 |
. . . . . 6
    
            |
94 | 34, 84, 93 | 3eqtr4d 2220 |
. . . . 5
    
                |
95 | | eqimss 3209 |
. . . . 5
                   |
96 | 94, 95 | syl 14 |
. . . 4
    
                |
97 | 59, 58 | eqeltrd 2254 |
. . . . . . 7
 

      |
98 | | el2oss1o 6438 |
. . . . . . 7
        
  |
99 | 97, 98 | syl 14 |
. . . . . 6
 

      |
100 | 99 | adantr 276 |
. . . . 5
                 |
101 | 90 | adantr 276 |
. . . . . 6
                            |
102 | | simpr 110 |
. . . . . . 7
                   |
103 | 102 | iffalsed 3544 |
. . . . . 6
                        |
104 | 101, 103 | eqtrd 2210 |
. . . . 5
                 |
105 | 100, 104 | sseqtrrd 3194 |
. . . 4
                     |
106 | | exmiddc 836 |
. . . . 5
DECID                       |
107 | 80, 106 | syl 14 |
. . . 4
 

 
    
         |
108 | 96, 105, 107 | mpjaodan 798 |
. . 3
 

          |
109 | 108 | ralrimiva 2550 |
. 2
     
      |
110 | | fveq1 5510 |
. . . . 5
           |
111 | | fveq1 5510 |
. . . . 5
           |
112 | 110, 111 | sseq12d 3186 |
. . . 4
             
       |
113 | 112 | ralbidv 2477 |
. . 3
  
                    |
114 | | df-nninf 7113 |
. . 3
ℕ∞   
           |
115 | 113, 114 | elrab2 2896 |
. 2
 ℕ∞    
           |
116 | 32, 109, 115 | sylanbrc 417 |
1

ℕ∞ |