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

recs 
 recs       recs     |
2 | 1 | ibi 176 |
. 2

recs 
     recs    |
3 | | df-recs 6300 |
. . . . . 6
recs      
             |
4 | 3 | eleq2i 2244 |
. . . . 5
  
 recs 
       
              |
5 | | eluniab 3819 |
. . . . 5
  
                      
   
              |
6 | 4, 5 | bitri 184 |
. . . 4
  
 recs 
      
                |
7 | | fnop 5315 |
. . . . . . . . . . . . . 14
   
    |
8 | | rspe 2526 |
. . . . . . . . . . . . . . . 16
               
  
             |
9 | | tfrlem.1 |
. . . . . . . . . . . . . . . . . 18
 
               |
10 | 9 | abeq2i 2288 |
. . . . . . . . . . . . . . . . 17

  
             |
11 | | elssuni 3835 |
. . . . . . . . . . . . . . . . . 18
    |
12 | 9 | recsfval 6310 |
. . . . . . . . . . . . . . . . . 18
recs    |
13 | 11, 12 | sseqtrrdi 3204 |
. . . . . . . . . . . . . . . . 17
 recs    |
14 | 10, 13 | sylbir 135 |
. . . . . . . . . . . . . . . 16
              
recs    |
15 | 8, 14 | syl 14 |
. . . . . . . . . . . . . . 15
               
recs    |
16 | | fveq2 5511 |
. . . . . . . . . . . . . . . . . . . 20
           |
17 | | reseq2 4898 |
. . . . . . . . . . . . . . . . . . . . 21
       |
18 | 17 | fveq2d 5515 |
. . . . . . . . . . . . . . . . . . . 20
               |
19 | 16, 18 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . 19
           
             |
20 | 19 | rspcv 2837 |
. . . . . . . . . . . . . . . . . 18
  
                       |
21 | | fndm 5311 |
. . . . . . . . . . . . . . . . . . . . 21

  |
22 | 21 | eleq2d 2247 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
23 | 9 | tfrlem7 6312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
recs   |
24 | | funssfv 5537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  recs  recs   recs           |
25 | 23, 24 | mp3an1 1324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
recs 
 recs           |
26 | 25 | adantrl 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
recs 
 

  recs           |
27 | 21 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
28 | | onelss 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
29 | 27, 28 | syl6bir 164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
    |
30 | 29 | imp31 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
    |
31 | | fun2ssres 5255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  recs  recs   recs       |
32 | 31 | fveq2d 5515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  recs  recs      recs            |
33 | 23, 32 | mp3an1 1324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
recs 
    recs            |
34 | 30, 33 | sylan2 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
recs 
 

     recs            |
35 | 26, 34 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
recs 
 

   recs        recs   
             |
36 | 35 | exbiri 382 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 recs    

            recs        recs        |
37 | 36 | com3l 81 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
              recs 
recs        recs 
      |
38 | 37 | exp31 364 |
. . . . . . . . . . . . . . . . . . . . . 22
               recs 
recs        recs 
        |
39 | 38 | com34 83 |
. . . . . . . . . . . . . . . . . . . . 21
               recs  recs        recs 
        |
40 | 39 | com24 87 |
. . . . . . . . . . . . . . . . . . . 20
 
             recs 
recs        recs 
        |
41 | 22, 40 | sylbird 170 |
. . . . . . . . . . . . . . . . . . 19
 
             recs 
recs        recs 
        |
42 | 41 | com3l 81 |
. . . . . . . . . . . . . . . . . 18
               recs 
recs        recs 
        |
43 | 20, 42 | syld 45 |
. . . . . . . . . . . . . . . . 17
  
             recs 
recs        recs 
        |
44 | 43 | com24 87 |
. . . . . . . . . . . . . . . 16
                recs 
recs        recs 
        |
45 | 44 | imp4d 352 |
. . . . . . . . . . . . . . 15
                
 recs  recs        recs        |
46 | 15, 45 | mpdi 43 |
. . . . . . . . . . . . . 14
                
recs        recs 
     |
47 | 7, 46 | syl 14 |
. . . . . . . . . . . . 13
   
                 
recs        recs 
     |
48 | 47 | exp4d 369 |
. . . . . . . . . . . 12
   
                recs        recs         |
49 | 48 | ex 115 |
. . . . . . . . . . 11
    
              recs        recs          |
50 | 49 | com4r 86 |
. . . . . . . . . 10
                   recs        recs          |
51 | 50 | pm2.43i 49 |
. . . . . . . . 9
    
  
          recs        recs         |
52 | 51 | com3l 81 |
. . . . . . . 8
  



 
          recs        recs 
       |
53 | 52 | imp4a 349 |
. . . . . . 7
  


              recs        recs        |
54 | 53 | rexlimdv 2593 |
. . . . . 6
  

 
             recs        recs       |
55 | 54 | imp 124 |
. . . . 5
    
  
           
recs        recs 
    |
56 | 55 | exlimiv 1598 |
. . . 4
                      recs        recs      |
57 | 6, 56 | sylbi 121 |
. . 3
  
 recs  recs        recs      |
58 | 57 | exlimiv 1598 |
. 2
      recs  recs        recs      |
59 | 2, 58 | syl 14 |
1

recs 
recs        recs 
    |