Step | Hyp | Ref
| Expression |
1 | | dm0 4492 |
. . . . . . . . . 10
 |
2 | 1 | biantrur 287 |
. . . . . . . . 9
 
   |
3 | | vex 2554 |
. . . . . . . . . . . . . . . 16
 |
4 | | nsuceq0g 4121 |
. . . . . . . . . . . . . . . 16
   |
5 | 3, 4 | ax-mp 7 |
. . . . . . . . . . . . . . 15
 |
6 | 5 | nesymi 2245 |
. . . . . . . . . . . . . 14
 |
7 | 1 | eqeq1i 2044 |
. . . . . . . . . . . . . 14
   |
8 | 6, 7 | mtbir 595 |
. . . . . . . . . . . . 13
 |
9 | 8 | intnanr 838 |
. . . . . . . . . . . 12

          |
10 | 9 | a1i 9 |
. . . . . . . . . . 11
 
           |
11 | 10 | nrex 2405 |
. . . . . . . . . 10


          |
12 | 11 | biorfi 664 |
. . . . . . . . 9
      

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

              |
15 | 14 | abbii 2150 |
. . . . . . 7


                  |
16 | | abid2 2155 |
. . . . . . 7


 |
17 | 15, 16 | eqtr3i 2059 |
. . . . . 6
                  |
18 | | elex 2560 |
. . . . . 6
   |
19 | 17, 18 | syl5eqel 2121 |
. . . . 5
 
 

               |
20 | | 0ex 3875 |
. . . . . . 7
 |
21 | | dmeq 4478 |
. . . . . . . . . . . . 13

  |
22 | 21 | eqeq1d 2045 |
. . . . . . . . . . . 12

    |
23 | | fveq1 5120 |
. . . . . . . . . . . . . 14

          |
24 | 23 | fveq2d 5125 |
. . . . . . . . . . . . 13

                  |
25 | 24 | eleq2d 2104 |
. . . . . . . . . . . 12


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

                        |
27 | 26 | rexbidv 2321 |
. . . . . . . . . 10

 
                        |
28 | 21 | eqeq1d 2045 |
. . . . . . . . . . 11

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

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

                 

               |
31 | 30 | abbidv 2152 |
. . . . . . . 8

                   

               |
32 | | eqid 2037 |
. . . . . . . 8
                  
                    |
33 | 31, 32 | fvmptg 5191 |
. . . . . . 7
  
 

               

 
                  
 

               |
34 | 20, 33 | mpan 400 |
. . . . . 6
 
 

                 

                 
 

               |
35 | 34, 17 | syl6eq 2085 |
. . . . 5
 
 

                 

                   |
36 | 19, 35 | syl 14 |
. . . 4
  

 
                    |
37 | 36, 18 | eqeltrd 2111 |
. . 3
  

 
                    |
38 | | df-frec 5918 |
. . . . . 6
frec   recs                    
  |
39 | 38 | fveq1i 5122 |
. . . . 5
frec 
     recs                    
     |
40 | | peano1 4260 |
. . . . . 6
 |
41 | | fvres 5141 |
. . . . . 6
  recs                    
    recs                          |
42 | 40, 41 | ax-mp 7 |
. . . . 5
 recs                    
    recs                         |
43 | 39, 42 | eqtri 2057 |
. . . 4
frec 
    recs                         |
44 | | eqid 2037 |
. . . . 5
recs    

              
recs 

 
                 |
45 | 44 | tfr0 5878 |
. . . 4
   
 
                  recs                                                 |
46 | 43, 45 | syl5eq 2081 |
. . 3
   
 
                  frec                               |
47 | 37, 46 | syl 14 |
. 2
 frec        
 
                    |
48 | 47, 36 | eqtrd 2069 |
1
 frec        |