Step | Hyp | Ref
| Expression |
1 | | eldm2g 4474 |
. . 3

recs   recs       recs     |
2 | 1 | ibi 165 |
. 2

recs       recs    |
3 | | df-recs 5861 |
. . . . . 6
recs   
  
             |
4 | 3 | eleq2i 2101 |
. . . . 5
    recs 
    
  
              |
5 | | eluniab 3583 |
. . . . 5
     

 
                  
 
              |
6 | 4, 5 | bitri 173 |
. . . 4
    recs 
      
 
              |
7 | | fnop 4945 |
. . . . . . . . . . . . . 14
   
    |
8 | | rspe 2364 |
. . . . . . . . . . . . . . . 16
  
        
    

        
     |
9 | | tfrlem.1 |
. . . . . . . . . . . . . . . . . 18


 
             |
10 | 9 | abeq2i 2145 |
. . . . . . . . . . . . . . . . 17
   
             |
11 | | elssuni 3599 |
. . . . . . . . . . . . . . . . . 18
    |
12 | 9 | recsfval 5872 |
. . . . . . . . . . . . . . . . . 18
recs    |
13 | 11, 12 | syl6sseqr 2986 |
. . . . . . . . . . . . . . . . 17
 recs    |
14 | 10, 13 | sylbir 125 |
. . . . . . . . . . . . . . . 16
 
 
           recs    |
15 | 8, 14 | syl 14 |
. . . . . . . . . . . . . . 15
  
        
    recs    |
16 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . . . 20
           |
17 | | reseq2 4550 |
. . . . . . . . . . . . . . . . . . . . 21
       |
18 | 17 | fveq2d 5125 |
. . . . . . . . . . . . . . . . . . . 20
               |
19 | 16, 18 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . . . 19
         
     
         |
20 | 19 | rspcv 2646 |
. . . . . . . . . . . . . . . . . 18
  
       
               |
21 | | fndm 4941 |
. . . . . . . . . . . . . . . . . . . . 21

  |
22 | 21 | eleq2d 2104 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
23 | 9 | tfrlem7 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
recs   |
24 | | funssfv 5142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  recs 
recs   recs    
      |
25 | 23, 24 | mp3an1 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
recs  
recs    
      |
26 | 25 | adantrl 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
recs       recs           |
27 | 21 | eleq1d 2103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
28 | | onelss 4090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
29 | 27, 28 | syl6bir 153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

    |
30 | 29 | imp31 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
 
  |
31 | | fun2ssres 4886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  recs 
recs   recs       |
32 | 31 | fveq2d 5125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  recs 
recs      recs 
          |
33 | 23, 32 | mp3an1 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
recs  
   recs 
          |
34 | 30, 33 | sylan2 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
recs          recs            |
35 | 26, 34 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
recs        recs        recs                 |
36 | 35 | exbiri 364 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 recs           
      recs    
   recs        |
37 | 36 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 
        
   recs  recs    
   recs 
      |
38 | 37 | exp31 346 |
. . . . . . . . . . . . . . . . . . . . . 22
 

            recs  recs    
   recs          |
39 | 38 | com34 77 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
       
recs  recs    
   recs          |
40 | 39 | com24 81 |
. . . . . . . . . . . . . . . . . . . 20
 
    
        recs  recs        recs          |
41 | 22, 40 | sylbird 159 |
. . . . . . . . . . . . . . . . . . 19
 
    
        recs  recs        recs          |
42 | 41 | com3l 75 |
. . . . . . . . . . . . . . . . . 18
         
   

recs  recs    
   recs          |
43 | 20, 42 | syld 40 |
. . . . . . . . . . . . . . . . 17
  
       
   

recs  recs    
   recs          |
44 | 43 | com24 81 |
. . . . . . . . . . . . . . . 16
 

     
      
recs  recs    
   recs          |
45 | 44 | imp4d 334 |
. . . . . . . . . . . . . . 15
  
         
    
recs  recs    
   recs        |
46 | 15, 45 | mpdi 38 |
. . . . . . . . . . . . . 14
  
         
    recs    
   recs 
     |
47 | 7, 46 | syl 14 |
. . . . . . . . . . . . 13
   
   
         
    recs    
   recs 
     |
48 | 47 | exp4d 351 |
. . . . . . . . . . . 12
   
  

     
      recs    
   recs 
       |
49 | 48 | ex 108 |
. . . . . . . . . . 11
        
       
  recs    
   recs          |
50 | 49 | com4r 80 |
. . . . . . . . . 10
        
       
  recs    
   recs          |
51 | 50 | pm2.43i 43 |
. . . . . . . . 9
       
       
  recs    
   recs         |
52 | 51 | com3l 75 |
. . . . . . . 8
           
      recs    
   recs 
       |
53 | 52 | imp4a 331 |
. . . . . . 7
       
           recs        recs        |
54 | 53 | rexlimdv 2426 |
. . . . . 6
       
           recs        recs       |
55 | 54 | imp 115 |
. . . . 5
       
            recs    
   recs      |
56 | 55 | exlimiv 1486 |
. . . 4
       
 
            recs    
   recs      |
57 | 6, 56 | sylbi 114 |
. . 3
    recs 
recs    
   recs      |
58 | 57 | exlimiv 1486 |
. 2
      recs  recs        recs      |
59 | 2, 58 | syl 14 |
1

recs  recs        recs      |