Step | Hyp | Ref
| Expression |
1 | | nninfsel.n |
. 2
   |
2 | | elequ2 1674 |
. . . . . . . 8
 
   |
3 | 2 | ifbid 3459 |
. . . . . . 7
             |
4 | 3 | mpteq2dv 3979 |
. . . . . 6
                 |
5 | 4 | fveq2d 5379 |
. . . . 5
                         |
6 | 5 | eqeq1d 2123 |
. . . 4
            
              |
7 | 6 | imbi2d 229 |
. . 3
  
           
                |
8 | | eleq2 2178 |
. . . . . . . 8
 
   |
9 | 8 | ifbid 3459 |
. . . . . . 7
             |
10 | 9 | mpteq2dv 3979 |
. . . . . 6
                 |
11 | 10 | fveq2d 5379 |
. . . . 5
                         |
12 | 11 | eqeq1d 2123 |
. . . 4
            
              |
13 | 12 | imbi2d 229 |
. . 3
  
           
                |
14 | | 1n0 6283 |
. . . . . . 7
 |
15 | 14 | neii 2284 |
. . . . . 6
 |
16 | | nninfsel.e |
. . . . . . . . . . . 12
 
ℕ∞    
             
    |
17 | | elequ2 1674 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
18 | 17 | ifbid 3459 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
19 | 18 | mpteq2dv 3979 |
. . . . . . . . . . . . . . . . . . 19
                 |
20 | 19 | fveq2d 5379 |
. . . . . . . . . . . . . . . . . 18
                         |
21 | 20 | eqeq1d 2123 |
. . . . . . . . . . . . . . . . 17
                           |
22 | 21 | cbvralv 2628 |
. . . . . . . . . . . . . . . 16
 
           
               |
23 | | elequ1 1673 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
24 | 23 | ifbid 3459 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
25 | 24 | cbvmptv 3984 |
. . . . . . . . . . . . . . . . . . 19
               |
26 | 25 | fveq2i 5378 |
. . . . . . . . . . . . . . . . . 18
                       |
27 | 26 | eqeq1i 2122 |
. . . . . . . . . . . . . . . . 17
           
             |
28 | 27 | ralbii 2415 |
. . . . . . . . . . . . . . . 16
 
           
               |
29 | 22, 28 | bitri 183 |
. . . . . . . . . . . . . . 15
 
           
               |
30 | | ifbi 3458 |
. . . . . . . . . . . . . . 15
                                                                   |
31 | 29, 30 | ax-mp 7 |
. . . . . . . . . . . . . 14
                                     |
32 | 31 | mpteq2i 3975 |
. . . . . . . . . . . . 13
                                         |
33 | 32 | mpteq2i 3975 |
. . . . . . . . . . . 12
  ℕ∞                       
ℕ∞    
             
    |
34 | 16, 33 | eqtri 2135 |
. . . . . . . . . . 11
 
ℕ∞    
             
    |
35 | | nninfsel.q |
. . . . . . . . . . . 12
  ℕ∞  |
36 | 35 | ad2antlr 478 |
. . . . . . . . . . 11
   

                           
ℕ∞  |
37 | | nninfsel.1 |
. . . . . . . . . . . 12
           |
38 | 37 | ad2antlr 478 |
. . . . . . . . . . 11
   

                                     |
39 | | simpll 501 |
. . . . . . . . . . . 12
    
             
  |
40 | 39 | adantr 272 |
. . . . . . . . . . 11
   

                             |
41 | | simpr 109 |
. . . . . . . . . . . . . 14
    
             
  |
42 | | simplr 502 |
. . . . . . . . . . . . . . 15
    
             

               |
43 | | r19.21v 2483 |
. . . . . . . . . . . . . . 15
 
            
                |
44 | 42, 43 | sylib 121 |
. . . . . . . . . . . . . 14
    
             
                |
45 | 41, 44 | mpd 13 |
. . . . . . . . . . . . 13
    
             

             |
46 | 25 | fveq2i 5378 |
. . . . . . . . . . . . . . 15
                       |
47 | 46 | eqeq1i 2122 |
. . . . . . . . . . . . . 14
           
             |
48 | 47 | ralbii 2415 |
. . . . . . . . . . . . 13
 
          

             |
49 | 45, 48 | sylib 121 |
. . . . . . . . . . . 12
    
             

             |
50 | 49 | adantr 272 |
. . . . . . . . . . 11
   

                           
             |
51 | | elequ1 1673 |
. . . . . . . . . . . . . . 15
 
   |
52 | 51 | ifbid 3459 |
. . . . . . . . . . . . . 14
             |
53 | 52 | cbvmptv 3984 |
. . . . . . . . . . . . 13
               |
54 | 53 | fveq2i 5378 |
. . . . . . . . . . . 12
                       |
55 | | simpr 109 |
. . . . . . . . . . . 12
   

                                        |
56 | 54, 55 | syl5eqr 2161 |
. . . . . . . . . . 11
   

                                        |
57 | 34, 36, 38, 40, 50, 56 | nninfsellemeq 12902 |
. . . . . . . . . 10
   

                                        |
58 | 57, 53 | syl6eqr 2165 |
. . . . . . . . 9
   

                                        |
59 | 58 | fveq2d 5379 |
. . . . . . . 8
   

                                                |
60 | 59, 38, 55 | 3eqtr3d 2155 |
. . . . . . 7
   

                             |
61 | 60 | ex 114 |
. . . . . 6
    
             
           
   |
62 | 15, 61 | mtoi 636 |
. . . . 5
    
             
             |
63 | 35 | adantl 273 |
. . . . . . . . . 10
    
             

ℕ∞  |
64 | | elmapi 6518 |
. . . . . . . . . 10
  ℕ∞  ℕ∞   |
65 | 63, 64 | syl 14 |
. . . . . . . . 9
    
             
 ℕ∞   |
66 | | nnnninf 6973 |
. . . . . . . . . 10
        ℕ∞ |
67 | 39, 66 | syl 14 |
. . . . . . . . 9
    
             
       ℕ∞ |
68 | 65, 67 | ffvelrnd 5510 |
. . . . . . . 8
    
             
             |
69 | | df2o3 6281 |
. . . . . . . 8
    |
70 | 68, 69 | syl6eleq 2207 |
. . . . . . 7
    
             
                |
71 | | elpri 3516 |
. . . . . . 7
                                         |
72 | 70, 71 | syl 14 |
. . . . . 6
    
             
           
              |
73 | 72 | orcomd 701 |
. . . . 5
    
             
                          |
74 | 62, 73 | ecased 1310 |
. . . 4
    
             
             |
75 | 74 | exp31 359 |
. . 3
  

                            |
76 | 7, 13, 75 | omsinds 4495 |
. 2
                |
77 | 1, 76 | mpcom 36 |
1
              |