Step | Hyp | Ref
| Expression |
1 | | dm0 4549 |
. . . . . . . . . 10
 |
2 | 1 | biantrur 287 |
. . . . . . . . 9


   |
3 | | vex 2560 |
. . . . . . . . . . . . . . . 16
 |
4 | | nsuceq0g 4155 |
. . . . . . . . . . . . . . . 16
   |
5 | 3, 4 | ax-mp 7 |
. . . . . . . . . . . . . . 15
 |
6 | 5 | nesymi 2251 |
. . . . . . . . . . . . . 14
 |
7 | 1 | eqeq1i 2047 |
. . . . . . . . . . . . . 14

  |
8 | 6, 7 | mtbir 596 |
. . . . . . . . . . . . 13
 |
9 | 8 | intnanr 839 |
. . . . . . . . . . . 12

          |
10 | 9 | a1i 9 |
. . . . . . . . . . 11
 
           |
11 | 10 | nrex 2411 |
. . . . . . . . . 10


          |
12 | 11 | biorfi 665 |
. . . . . . . . 9
  
   

            |
13 | | orcom 647 |
. . . . . . . . 9
                                 |
14 | 2, 12, 13 | 3bitri 195 |
. . . . . . . 8

 

              |
15 | 14 | abbii 2153 |
. . . . . . 7


                  |
16 | | abid2 2158 |
. . . . . . 7


 |
17 | 15, 16 | eqtr3i 2062 |
. . . . . 6
                  |
18 | | elex 2566 |
. . . . . 6
   |
19 | 17, 18 | syl5eqel 2124 |
. . . . 5
                    |
20 | | 0ex 3884 |
. . . . . . 7
 |
21 | | dmeq 4535 |
. . . . . . . . . . . . 13

  |
22 | 21 | eqeq1d 2048 |
. . . . . . . . . . . 12

    |
23 | | fveq1 5177 |
. . . . . . . . . . . . . 14

          |
24 | 23 | fveq2d 5182 |
. . . . . . . . . . . . 13

                  |
25 | 24 | eleq2d 2107 |
. . . . . . . . . . . 12

        
           |
26 | 22, 25 | anbi12d 442 |
. . . . . . . . . . 11

                        |
27 | 26 | rexbidv 2327 |
. . . . . . . . . 10

  
          
            |
28 | 21 | eqeq1d 2048 |
. . . . . . . . . . 11


   |
29 | 28 | anbi1d 438 |
. . . . . . . . . 10

   
    |
30 | 27, 29 | orbi12d 707 |
. . . . . . . . 9

               
 

               |
31 | 30 | abbidv 2155 |
. . . . . . . 8

             
                      |
32 | | eqid 2040 |
. . . . . . . 8
              
                  
     |
33 | 31, 32 | fvmptg 5248 |
. . . . . . 7
 
   
                             
          
               |
34 | 20, 33 | mpan 400 |
. . . . . 6
    
                            
          
               |
35 | 34, 17 | syl6eq 2088 |
. . . . 5
    
                            
         |
36 | 19, 35 | syl 14 |
. . . 4
   
 
                    |
37 | 36, 18 | eqeltrd 2114 |
. . 3
   
 
                    |
38 | | df-frec 5978 |
. . . . . 6
frec   recs               
       |
39 | 38 | fveq1i 5179 |
. . . . 5
frec       recs               
          |
40 | | peano1 4317 |
. . . . . 6
 |
41 | | fvres 5198 |
. . . . . 6

 recs               
         recs               
          |
42 | 40, 41 | ax-mp 7 |
. . . . 5
 recs               
         recs               
         |
43 | 39, 42 | eqtri 2060 |
. . . 4
frec      recs               
         |
44 | | eqid 2040 |
. . . . 5
recs     
               recs  
 
                 |
45 | 44 | tfr0 5937 |
. . . 4
   
 
                  recs     
                                 
         |
46 | 43, 45 | syl5eq 2084 |
. . 3
   
 
                  frec           
                   |
47 | 37, 46 | syl 14 |
. 2
 frec        
 
                    |
48 | 47, 36 | eqtrd 2072 |
1
 frec        |