Step | Hyp | Ref
| Expression |
1 | | elun 3574 |
. . . . . 6
    
  
        
      

   
          |
2 | | predel 5397 |
. . . . . . . . . . 11
    
   |
3 | | setlikespec 5401 |
. . . . . . . . . . . . . 14
  Se    
    |
4 | | trpredpred 30469 |
. . . . . . . . . . . . . 14
         
        |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . . 13
  Se    
         |
6 | 5 | expcom 437 |
. . . . . . . . . . . 12
 Se

  
          |
7 | 6 | adantl 468 |
. . . . . . . . . . 11
  Se                |
8 | 2, 7 | syl5 33 |
. . . . . . . . . 10
  Se     
    
          |
9 | 8 | ancld 556 |
. . . . . . . . 9
  Se     
     
                |
10 | | trpredeq3 30463 |
. . . . . . . . . . . 12
             |
11 | 10 | sseq2d 3460 |
. . . . . . . . . . 11
           
    
        |
12 | 11 | rspcev 3150 |
. . . . . . . . . 10
    
                
              |
13 | | ssiun 4320 |
. . . . . . . . . 10
   
     
      
    
   
         |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
    
               
     
         |
15 | 9, 14 | syl6 34 |
. . . . . . . 8
  Se     
    
     
          |
16 | | eliun 4283 |
. . . . . . . . 9
    
      
   
         |
17 | | predel 5397 |
. . . . . . . . . . . 12
    
   |
18 | | setlikespec 5401 |
. . . . . . . . . . . . . . . . . . . . 21
  Se    
    |
19 | 18 | ancoms 455 |
. . . . . . . . . . . . . . . . . . . 20
  Se    
    |
20 | 19 | adantll 720 |
. . . . . . . . . . . . . . . . . . 19
  
Se 

       |
21 | | trpredss 30470 |
. . . . . . . . . . . . . . . . . . 19
         
   |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
Se 

    
  |
23 | 22 | sseld 3431 |
. . . . . . . . . . . . . . . . 17
  
Se 

    
    |
24 | 3 | expcom 437 |
. . . . . . . . . . . . . . . . . 18
 Se

  
     |
25 | 24 | ad2antlr 733 |
. . . . . . . . . . . . . . . . 17
  
Se 


  
     |
26 | 23, 25 | syld 45 |
. . . . . . . . . . . . . . . 16
  
Se 

    
    
    |
27 | 26 | imp 431 |
. . . . . . . . . . . . . . 15
    Se 
    
 
       |
28 | 27, 4 | syl 17 |
. . . . . . . . . . . . . 14
    Se 
    
 
    
       |
29 | | simpr 463 |
. . . . . . . . . . . . . . . 16
  
Se 

  |
30 | | simplr 762 |
. . . . . . . . . . . . . . . 16
  
Se 

Se   |
31 | | trpredelss 30473 |
. . . . . . . . . . . . . . . 16
  Se       
    
        |
32 | 29, 30, 31 | syl2anc 667 |
. . . . . . . . . . . . . . 15
  
Se 

    
              |
33 | 32 | imp 431 |
. . . . . . . . . . . . . 14
    Se 
    
 
    
       |
34 | 28, 33 | sstrd 3442 |
. . . . . . . . . . . . 13
    Se 
    
 
    
       |
35 | 34 | exp31 609 |
. . . . . . . . . . . 12
  Se           
           |
36 | 17, 35 | syl5 33 |
. . . . . . . . . . 11
  Se     
       
    
         |
37 | 36 | reximdvai 2859 |
. . . . . . . . . 10
  Se   
          
       
          |
38 | 37, 13 | syl6 34 |
. . . . . . . . 9
  Se   
                 
           |
39 | 16, 38 | syl5bi 221 |
. . . . . . . 8
  Se      
              
           |
40 | 15, 39 | jaod 382 |
. . . . . . 7
  Se                       
     
          |
41 | | ssun4 3600 |
. . . . . . 7
        
       
    
      
        
    |
42 | 40, 41 | syl6 34 |
. . . . . 6
  Se                       
        
        
     |
43 | 1, 42 | syl5bi 221 |
. . . . 5
  Se         
        
 
    
      
        
     |
44 | 43 | ralrimiv 2800 |
. . . 4
  Se            
            
          
          |
45 | | ssun1 3597 |
. . . 4
  
        
        
   |
46 | 44, 45 | jctir 541 |
. . 3
  Se   
      
        
      
          
           
          
           |
47 | | trpredmintr 30472 |
. . 3
  
Se             
            
          
           
          
              
      
        
    |
48 | 46, 47 | mpdan 674 |
. 2
  Se      
      
        
    |
49 | | setlikespec 5401 |
. . . 4
  Se    
    |
50 | | trpredpred 30469 |
. . . 4
         
        |
51 | 49, 50 | syl 17 |
. . 3
  Se    
         |
52 | 51 | sseld 3431 |
. . . . . 6
  Se     
     
    |
53 | | trpredelss 30473 |
. . . . . 6
  Se       
    
        |
54 | 52, 53 | syld 45 |
. . . . 5
  Se     
      
        |
55 | 54 | ralrimiv 2800 |
. . . 4
  Se     
              |
56 | | iunss 4319 |
. . . 4
 
        
     
   
              |
57 | 55, 56 | sylibr 216 |
. . 3
  Se     
              |
58 | 51, 57 | unssd 3610 |
. 2
  Se        
        
 
       |
59 | 48, 58 | eqssd 3449 |
1
  Se             
        
    |