Step | Hyp | Ref
| Expression |
1 | | 1n0 6432 |
. . . . 5
 |
2 | 1 | nesymi 2393 |
. . . 4
 |
3 | | simplr 528 |
. . . . . . . . . . 11
   ℕ∞     
ℕ∞ |
4 | | nninff 7120 |
. . . . . . . . . . . 12
 ℕ∞       |
5 | 4 | ffnd 5366 |
. . . . . . . . . . 11
 ℕ∞   |
6 | 3, 5 | syl 14 |
. . . . . . . . . 10
   ℕ∞        |
7 | | nninfall.q |
. . . . . . . . . . . . . . 15
  ℕ∞  |
8 | 7 | ad2antrr 488 |
. . . . . . . . . . . . . 14
   ℕ∞      
ℕ∞  |
9 | | nninfall.inf |
. . . . . . . . . . . . . . 15
         |
10 | 9 | ad2antrr 488 |
. . . . . . . . . . . . . 14
   ℕ∞         
    |
11 | | nninfall.n |
. . . . . . . . . . . . . . 15
               |
12 | 11 | ad2antrr 488 |
. . . . . . . . . . . . . 14
   ℕ∞                    |
13 | | simpr 110 |
. . . . . . . . . . . . . 14
   ℕ∞            |
14 | 8, 10, 12, 3, 13 | nninfalllem1 14727 |
. . . . . . . . . . . . 13
   ℕ∞             |
15 | | eqeq1 2184 |
. . . . . . . . . . . . . . 15
     
       |
16 | 15 | ralrn 5654 |
. . . . . . . . . . . . . 14
  
        |
17 | 3, 5, 16 | 3syl 17 |
. . . . . . . . . . . . 13
   ℕ∞                |
18 | 14, 17 | mpbird 167 |
. . . . . . . . . . . 12
   ℕ∞      
  |
19 | | peano1 4593 |
. . . . . . . . . . . . . . . 16
 |
20 | | elex2 2753 |
. . . . . . . . . . . . . . . 16

   |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . 15
  |
22 | | fdm 5371 |
. . . . . . . . . . . . . . . . 17
       |
23 | 22 | eleq2d 2247 |
. . . . . . . . . . . . . . . 16
         |
24 | 23 | exbidv 1825 |
. . . . . . . . . . . . . . 15
      
    |
25 | 21, 24 | mpbiri 168 |
. . . . . . . . . . . . . 14
        |
26 | | dmmrnm 4846 |
. . . . . . . . . . . . . . 15
     |
27 | | eqsnm 3755 |
. . . . . . . . . . . . . . 15
    
    |
28 | 26, 27 | sylbi 121 |
. . . . . . . . . . . . . 14
    
    |
29 | 25, 28 | syl 14 |
. . . . . . . . . . . . 13
        
   |
30 | 3, 4, 29 | 3syl 17 |
. . . . . . . . . . . 12
   ℕ∞        
    |
31 | 18, 30 | mpbird 167 |
. . . . . . . . . . 11
   ℕ∞     
    |
32 | | eqimss 3209 |
. . . . . . . . . . 11
  
    |
33 | 31, 32 | syl 14 |
. . . . . . . . . 10
   ℕ∞     
    |
34 | | df-f 5220 |
. . . . . . . . . 10
             |
35 | 6, 33, 34 | sylanbrc 417 |
. . . . . . . . 9
   ℕ∞              |
36 | | 1onn 6520 |
. . . . . . . . . 10
 |
37 | | fconst2g 5731 |
. . . . . . . . . 10
               |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
             |
39 | 35, 38 | sylib 122 |
. . . . . . . 8
   ℕ∞            |
40 | | fconstmpt 4673 |
. . . . . . . 8
       |
41 | 39, 40 | eqtrdi 2226 |
. . . . . . 7
   ℕ∞          |
42 | 41 | fveq2d 5519 |
. . . . . 6
   ℕ∞                  |
43 | 42, 13, 10 | 3eqtr3d 2218 |
. . . . 5
   ℕ∞        |
44 | 43 | ex 115 |
. . . 4
 
ℕ∞         |
45 | 2, 44 | mtoi 664 |
. . 3
 
ℕ∞       |
46 | | elmapi 6669 |
. . . . . . 7
  ℕ∞  ℕ∞   |
47 | 7, 46 | syl 14 |
. . . . . 6
  ℕ∞   |
48 | 47 | ffvelcdmda 5651 |
. . . . 5
 
ℕ∞       |
49 | | elpri 3615 |
. . . . . 6
                    |
50 | | df2o3 6430 |
. . . . . 6
    |
51 | 49, 50 | eleq2s 2272 |
. . . . 5
                 |
52 | 48, 51 | syl 14 |
. . . 4
 
ℕ∞             |
53 | 52 | orcomd 729 |
. . 3
 
ℕ∞             |
54 | 45, 53 | ecased 1349 |
. 2
 
ℕ∞       |
55 | 54 | ralrimiva 2550 |
1
 
ℕ∞       |