Step | Hyp | Ref
| Expression |
1 | | fveq2 5516 |
. . . . . 6
           |
2 | 1 | eqeq1d 2186 |
. . . . 5
     
       |
3 | 2 | imbi2d 230 |
. . . 4
  
    
         |
4 | | fveq2 5516 |
. . . . . 6
           |
5 | 4 | eqeq1d 2186 |
. . . . 5
     
       |
6 | 5 | imbi2d 230 |
. . . 4
  
    
         |
7 | | 1n0 6433 |
. . . . . . . 8
 |
8 | 7 | nesymi 2393 |
. . . . . . 7
 |
9 | | nninfalllem1.p |
. . . . . . . . . . . 12

ℕ∞ |
10 | 9 | ad2antlr 489 |
. . . . . . . . . . 11
   

            
ℕ∞ |
11 | | simplll 533 |
. . . . . . . . . . 11
   

            
  |
12 | | simplr 528 |
. . . . . . . . . . . 12
   

               |
13 | | simpllr 534 |
. . . . . . . . . . . . 13
   

             

       |
14 | | r19.21v 2554 |
. . . . . . . . . . . . 13
 
               |
15 | 13, 14 | sylib 122 |
. . . . . . . . . . . 12
   

             

       |
16 | 12, 15 | mpd 13 |
. . . . . . . . . . 11
   

             
      |
17 | | simpr 110 |
. . . . . . . . . . 11
   

                   |
18 | 10, 11, 16, 17 | nnnninfeq 7126 |
. . . . . . . . . 10
   

            
         |
19 | 18 | fveq2d 5520 |
. . . . . . . . 9
   

                              |
20 | | nninfalllem1.n0 |
. . . . . . . . . 10
       |
21 | 20 | ad2antlr 489 |
. . . . . . . . 9
   

                   |
22 | | elequ2 2153 |
. . . . . . . . . . . . . 14
 
   |
23 | 22 | ifbid 3556 |
. . . . . . . . . . . . 13
             |
24 | 23 | mpteq2dv 4095 |
. . . . . . . . . . . 12
                 |
25 | 24 | fveq2d 5520 |
. . . . . . . . . . 11
                         |
26 | 25 | eqeq1d 2186 |
. . . . . . . . . 10
            
              |
27 | | nninfall.n |
. . . . . . . . . . 11
               |
28 | 27 | ad2antlr 489 |
. . . . . . . . . 10
   

             
             |
29 | 26, 28, 11 | rspcdva 2847 |
. . . . . . . . 9
   

                          |
30 | 19, 21, 29 | 3eqtr3d 2218 |
. . . . . . . 8
   

               |
31 | 30 | ex 115 |
. . . . . . 7
    
               |
32 | 8, 31 | mtoi 664 |
. . . . . 6
    
      
      |
33 | | fveq1 5515 |
. . . . . . . . . . . . . . . 16
           |
34 | | fveq1 5515 |
. . . . . . . . . . . . . . . 16
           |
35 | 33, 34 | sseq12d 3187 |
. . . . . . . . . . . . . . 15
             
       |
36 | 35 | ralbidv 2477 |
. . . . . . . . . . . . . 14
  
                    |
37 | | df-nninf 7119 |
. . . . . . . . . . . . . 14
ℕ∞   
           |
38 | 36, 37 | elrab2 2897 |
. . . . . . . . . . . . 13
 ℕ∞    
           |
39 | 9, 38 | sylib 122 |
. . . . . . . . . . . 12
        
       |
40 | 39 | simpld 112 |
. . . . . . . . . . 11
     |
41 | | elmapi 6670 |
. . . . . . . . . . 11
  
      |
42 | 40, 41 | syl 14 |
. . . . . . . . . 10
       |
43 | 42 | adantl 277 |
. . . . . . . . 9
    
             |
44 | | simpll 527 |
. . . . . . . . 9
    
         |
45 | 43, 44 | ffvelcdmd 5653 |
. . . . . . . 8
    
             |
46 | | elpri 3616 |
. . . . . . . . 9
                    |
47 | | df2o3 6431 |
. . . . . . . . 9
    |
48 | 46, 47 | eleq2s 2272 |
. . . . . . . 8
                 |
49 | 45, 48 | syl 14 |
. . . . . . 7
    
                   |
50 | 49 | orcomd 729 |
. . . . . 6
    
                   |
51 | 32, 50 | ecased 1349 |
. . . . 5
    
             |
52 | 51 | exp31 364 |
. . . 4
  

    
         |
53 | 3, 6, 52 | omsinds 4622 |
. . 3
         |
54 | 53 | impcom 125 |
. 2
 

      |
55 | 54 | ralrimiva 2550 |
1
        |