Step | Hyp | Ref
| Expression |
1 | | simpr 463 |
. . . . . . . . . . . 12
            
    |
2 | 1 | 2a1i 12 |
. . . . . . . . . . 11
 
     
            
      |
3 | | inss2 3652 |
. . . . . . . . . . . 12
   |
4 | 3 | sseli 3427 |
. . . . . . . . . . 11
     |
5 | 2, 4 | syl8 72 |
. . . . . . . . . 10
 
     
            
    |
6 | | inss1 3651 |
. . . . . . . . . . . . 13
   |
7 | 6 | sseli 3427 |
. . . . . . . . . . . 12
     |
8 | 2, 7 | syl8 72 |
. . . . . . . . . . 11
 
     
            
    |
9 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
   |
10 | | simpl 459 |
. . . . . . . . . . . . . . 15
    
  |
11 | | ssel 3425 |
. . . . . . . . . . . . . . 15

    |
12 | 9, 10, 11 | syl2im 39 |
. . . . . . . . . . . . . 14
 
     
   |
13 | | eloni 5432 |
. . . . . . . . . . . . . 14
   |
14 | 12, 13 | syl6 34 |
. . . . . . . . . . . . 13
 
     
   |
15 | | ordtr 5436 |
. . . . . . . . . . . . 13

  |
16 | 14, 15 | syl6 34 |
. . . . . . . . . . . 12
 
     
   |
17 | | simpll 759 |
. . . . . . . . . . . . . 14
            
    |
18 | 17 | 2a1i 12 |
. . . . . . . . . . . . 13
 
     
            
      |
19 | | inss2 3652 |
. . . . . . . . . . . . . 14
   |
20 | 19 | sseli 3427 |
. . . . . . . . . . . . 13
     |
21 | 18, 20 | syl8 72 |
. . . . . . . . . . . 12
 
     
            
    |
22 | | trel 4503 |
. . . . . . . . . . . . 13

 
    |
23 | 22 | expcomd 440 |
. . . . . . . . . . . 12


     |
24 | 16, 21, 5, 23 | ee233 36870 |
. . . . . . . . . . 11
 
     
            
    |
25 | | elin 3616 |
. . . . . . . . . . . 12
  

   |
26 | 25 | simplbi2 630 |
. . . . . . . . . . 11
       |
27 | 8, 24, 26 | ee33 36872 |
. . . . . . . . . 10
 
     
            
      |
28 | | elin 3616 |
. . . . . . . . . . 11
    
  
   |
29 | 28 | simplbi2com 632 |
. . . . . . . . . 10
           |
30 | 5, 27, 29 | ee33 36872 |
. . . . . . . . 9
 
     
            
        |
31 | 30 | exp4a 610 |
. . . . . . . 8
 
     
              
      |
32 | 31 | ggen31 36905 |
. . . . . . 7
 
     
             
         |
33 | | dfss2 3420 |
. . . . . . . 8
      
       
    |
34 | 33 | biimpri 210 |
. . . . . . 7
     
     
       |
35 | 32, 34 | syl8 72 |
. . . . . 6
 
     
          
 
      |
36 | | simpr 463 |
. . . . . . 7
               |
37 | 36 | 2a1i 12 |
. . . . . 6
 
     
                 |
38 | | sseq0 3765 |
. . . . . . 7
   
 
    
  
   |
39 | 38 | ex 436 |
. . . . . 6
            
    |
40 | 35, 37, 39 | ee33 36872 |
. . . . 5
 
     
               |
41 | | simpl 459 |
. . . . . . 7
             |
42 | 41 | 2a1i 12 |
. . . . . 6
 
     
               |
43 | | inss1 3651 |
. . . . . . 7
   |
44 | 43 | sseli 3427 |
. . . . . 6
     |
45 | 42, 44 | syl8 72 |
. . . . 5
 
     
             |
46 | | pm3.21 450 |
. . . . 5
  
        |
47 | 40, 45, 46 | ee33 36872 |
. . . 4
 
     
                 |
48 | 47 | alrimdv 1774 |
. . 3
 
     
     
 
           |
49 | | onfrALTlem3 36904 |
. . . 4
 
     
           |
50 | | df-rex 2742 |
. . . 4
       
        
    |
51 | 49, 50 | syl6ib 230 |
. . 3
 
     
             |
52 | | exim 1705 |
. . 3
         
                     
     |
53 | 48, 51, 52 | syl6c 66 |
. 2
 
     
         |
54 | | df-rex 2742 |
. 2
   
   
    |
55 | 53, 54 | syl6ibr 231 |
1
 
     

     |