Step | Hyp | Ref
| Expression |
1 | | eltrpred 27835 |
. 2
    
                  
        |
2 | | nn0suc 6611 |
. . . 4
  
   |
3 | | fveq2 5800 |
. . . . . . . . . . 11

     
                          
     
         |
4 | 3 | eleq2d 2524 |
. . . . . . . . . 10

          
     
            
                    |
5 | 4 | anbi2d 703 |
. . . . . . . . 9

  
Se 
     
          
      
 
Se                  
          |
6 | 5 | biimpd 207 |
. . . . . . . 8

  
Se 
     
          
         Se 
                
          |
7 | | setlikespec 27793 |
. . . . . . . . . . 11
  Se    
    |
8 | | fr0g 7002 |
. . . . . . . . . . 11
                      
        
    |
9 | 7, 8 | syl 16 |
. . . . . . . . . 10
  Se       
          
        
    |
10 | 9 | eleq2d 2524 |
. . . . . . . . 9
  Se  
         
     
      
        |
11 | 10 | biimpa 484 |
. . . . . . . 8
  
Se 
     
          
          
   |
12 | 6, 11 | syl6com 35 |
. . . . . . 7
  
Se 
     
          
          
     |
13 | | fveq2 5800 |
. . . . . . . . . . . . 13
                 
           
          
        |
14 | 13 | eleq2d 2524 |
. . . . . . . . . . . 12
       
          
     
                
         |
15 | 14 | anbi2d 703 |
. . . . . . . . . . 11
    Se                  
      
 
Se                  
          |
16 | 15 | biimpd 207 |
. . . . . . . . . 10
    Se                  
         Se 
                
          |
17 | | fvex 5810 |
. . . . . . . . . . . . . . . . 17
     
                  |
18 | | trpredlem1 27836 |
. . . . . . . . . . . . . . . . . . . . 21
                      
        |
19 | 7, 18 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
  Se       
          
        |
20 | 19 | sseld 3464 |
. . . . . . . . . . . . . . . . . . 19
  Se        
                    |
21 | | setlikespec 27793 |
. . . . . . . . . . . . . . . . . . . . 21
  Se    
    |
22 | 21 | expcom 435 |
. . . . . . . . . . . . . . . . . . . 20
 Se

  
     |
23 | 22 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
  Se           |
24 | 20, 23 | syld 44 |
. . . . . . . . . . . . . . . . . 18
  Se        
                    
    |
25 | 24 | ralrimiv 2828 |
. . . . . . . . . . . . . . . . 17
  Se                   
         
    |
26 | | iunexg 6664 |
. . . . . . . . . . . . . . . . 17
                  
            
          
         
         
          
         
    |
27 | 17, 25, 26 | sylancr 663 |
. . . . . . . . . . . . . . . 16
  Se                   
         
    |
28 | | nfcv 2616 |
. . . . . . . . . . . . . . . . 17
        |
29 | | nfcv 2616 |
. . . . . . . . . . . . . . . . 17
   |
30 | | nfmpt1 4490 |
. . . . . . . . . . . . . . . . . . . . 21
           |
31 | 30, 28 | nfrdg 6981 |
. . . . . . . . . . . . . . . . . . . 20
         
     
    |
32 | | nfcv 2616 |
. . . . . . . . . . . . . . . . . . . 20
   |
33 | 31, 32 | nfres 5221 |
. . . . . . . . . . . . . . . . . . 19
      
          
    |
34 | 33, 29 | nffv 5807 |
. . . . . . . . . . . . . . . . . 18
                  
       |
35 | | nfcv 2616 |
. . . . . . . . . . . . . . . . . 18
        |
36 | 34, 35 | nfiun 4307 |
. . . . . . . . . . . . . . . . 17
  
     
          
         
   |
37 | | eqid 2454 |
. . . . . . . . . . . . . . . . 17
        
     
   
        
     
     |
38 | | predeq3 27774 |
. . . . . . . . . . . . . . . . . . 19
   
         |
39 | 38 | cbviunv 4318 |
. . . . . . . . . . . . . . . . . 18

     
      |
40 | | iuneq1 4293 |
. . . . . . . . . . . . . . . . . 18
          
     
           
       
          
         
    |
41 | 39, 40 | syl5eq 2507 |
. . . . . . . . . . . . . . . . 17
          
     
           
       
          
         
    |
42 | 28, 29, 36, 37, 41 | frsucmpt 7004 |
. . . . . . . . . . . . . . . 16
        
                     
       
          
      
         
     
           
   |
43 | 27, 42 | sylan2 474 |
. . . . . . . . . . . . . . 15
  
Se  
         
     
                        
         
    |
44 | 43 | eleq2d 2524 |
. . . . . . . . . . . . . 14
  
Se  
                 
     
      
                     
    |
45 | 44 | biimpd 207 |
. . . . . . . . . . . . 13
  
Se  
                 
            
          
         
     |
46 | 45 | expimpd 603 |
. . . . . . . . . . . 12
    Se 
                
      
                 
         
     |
47 | | eliun 4284 |
. . . . . . . . . . . . 13
                  
         
 
                 
          
   |
48 | | ssiun2 4322 |
. . . . . . . . . . . . . . . . . 18
      
          
                
     
         |
49 | | dftrpred2 27828 |
. . . . . . . . . . . . . . . . . 18
               
     
        |
50 | 48, 49 | syl6sseqr 3512 |
. . . . . . . . . . . . . . . . 17
      
          
             |
51 | 50 | sseld 3464 |
. . . . . . . . . . . . . . . 16
       
                         |
52 | | vex 3081 |
. . . . . . . . . . . . . . . . . 18
 |
53 | 52 | elpredim 27782 |
. . . . . . . . . . . . . . . . 17
    
     |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
    
     |
55 | 51, 54 | anim12d 563 |
. . . . . . . . . . . . . . 15
        
          
         
 
    
       |
56 | 55 | reximdv2 2931 |
. . . . . . . . . . . . . 14
  
     
          
          
            |
57 | 56 | com12 31 |
. . . . . . . . . . . . 13
       
                    
              |
58 | 47, 57 | sylbi 195 |
. . . . . . . . . . . 12
                  
         
              |
59 | 46, 58 | syl6com 35 |
. . . . . . . . . . 11
  
Se 
     
          
                     |
60 | 59 | pm2.43d 48 |
. . . . . . . . . 10
  
Se 
     
          
                   |
61 | 16, 60 | syl6com 35 |
. . . . . . . . 9
  
Se 
     
          
                     |
62 | 61 | com23 78 |
. . . . . . . 8
  
Se 
     
          
                     |
63 | 62 | rexlimdv 2946 |
. . . . . . 7
  
Se 
     
          
                    |
64 | 12, 63 | orim12d 834 |
. . . . . 6
  
Se 
     
          
           
        
        |
65 | 64 | ex 434 |
. . . . 5
  Se  
         
     
        
  
        
         |
66 | 65 | com23 78 |
. . . 4
  Se    
                  
      
        
         |
67 | 2, 66 | syl5 32 |
. . 3
  Se         
                     
              |
68 | 67 | rexlimdv 2946 |
. 2
  Se   
         
     
           
             |
69 | 1, 68 | syl5bi 217 |
1
  Se  
    
    
             |