Step | Hyp | Ref
| Expression |
1 | | ineq1 3627 |
. . . . 5
 
     |
2 | 1 | eleq1d 2513 |
. . . 4
   
     |
3 | 2 | imbi2d 318 |
. . 3
                  
   
 
 

 
           
         |
4 | | elgrug 9217 |
. . . . . 6


            
     |
5 | 4 | ibi 245 |
. . . . 5

 
 
    
   
    |
6 | | trin 4507 |
. . . . . . 7
   
   |
7 | 6 | ex 436 |
. . . . . 6


     |
8 | | inss1 3652 |
. . . . . . . 8
   |
9 | | ssralv 3493 |
. . . . . . . 8
    
          

     

            |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
 
 
        

     

           |
11 | | inss2 3653 |
. . . . . . . 8
   |
12 | | ssralv 3493 |
. . . . . . . 8
    
             
 
     

                |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
 
 
           
 
     

               |
14 | | elin 3617 |
. . . . . . . . . . . . 13
   
 

   |
15 | 14 | simplbi2 631 |
. . . . . . . . . . . 12
   
      |
16 | | ssralv 3493 |
. . . . . . . . . . . . . 14
    
   

        |
17 | 8, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
 
            |
18 | | ssralv 3493 |
. . . . . . . . . . . . . 14
    
   

        |
19 | 11, 18 | ax-mp 5 |
. . . . . . . . . . . . 13
 
            |
20 | | elin 3617 |
. . . . . . . . . . . . . . 15
     
          |
21 | 20 | simplbi2 631 |
. . . . . . . . . . . . . 14
                |
22 | 21 | ral2imi 2776 |
. . . . . . . . . . . . 13
 
                          |
23 | 17, 19, 22 | syl2im 39 |
. . . . . . . . . . . 12
 
    
   

          |
24 | 15, 23 | im2anan9 846 |
. . . . . . . . . . 11
                   
             |
25 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
26 | | mapss 7514 |
. . . . . . . . . . . . . 14
  
     
    |
27 | 25, 8, 26 | mp2an 678 |
. . . . . . . . . . . . 13
    
  |
28 | | ssralv 3493 |
. . . . . . . . . . . . 13
   
  
 
   
      
   |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . 12
 
   
      
  |
30 | 25 | inex1 4544 |
. . . . . . . . . . . . . . . . 17
   |
31 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
32 | 30, 31 | elmap 7500 |
. . . . . . . . . . . . . . . 16
    
        |
33 | | fss 5737 |
. . . . . . . . . . . . . . . . 17
        
        |
34 | 11, 33 | mpan2 677 |
. . . . . . . . . . . . . . . 16
             |
35 | 32, 34 | sylbi 199 |
. . . . . . . . . . . . . . 15
           |
36 | 35 | imim1i 60 |
. . . . . . . . . . . . . 14
       
    
    |
37 | 36 | alimi 1684 |
. . . . . . . . . . . . 13
        
        
   |
38 | | df-ral 2742 |
. . . . . . . . . . . . 13
 
 
   
     
     |
39 | 37, 38 | sylibr 216 |
. . . . . . . . . . . 12
        
    
     |
40 | | elin 3617 |
. . . . . . . . . . . . . 14
 

   
   |
41 | 40 | simplbi2 631 |
. . . . . . . . . . . . 13
 
 

     |
42 | 41 | ral2imi 2776 |
. . . . . . . . . . . 12
 
 
   
    
      
        |
43 | 29, 39, 42 | syl2im 39 |
. . . . . . . . . . 11
 
   
         
            |
44 | 24, 43 | im2anan9 846 |
. . . . . . . . . 10
    
    
   
                 
 
  

                        |
45 | 44 | 3impa 1203 |
. . . . . . . . 9
           

    
           
 
  

                        |
46 | | df-3an 987 |
. . . . . . . . 9
              
                 
    |
47 | | df-3an 987 |
. . . . . . . . 9
                       
  

                       |
48 | 45, 46, 47 | 3imtr4g 274 |
. . . . . . . 8
           

  
           
 
 
  
      
              |
49 | 48 | ral2imi 2776 |
. . . . . . 7
 
         
   
       

                    
                      |
50 | 10, 13, 49 | syl2im 39 |
. . . . . 6
 
 
        

 
 
           
 
       
                      |
51 | 7, 50 | im2anan9 846 |
. . . . 5
  
 
        
                  
     
       
                       |
52 | 5, 51 | syl 17 |
. . . 4

  
 
           
     
       
                       |
53 | | elgrug 9217 |
. . . . 5
     
 
        
                       |
54 | 30, 53 | ax-mp 5 |
. . . 4
  
 
        
                      |
55 | 52, 54 | syl6ibr 231 |
. . 3

  
 
           
   
    |
56 | 3, 55 | vtoclga 3113 |
. 2

  
 
           
        |
57 | 56 | com12 32 |
1
  
 
           
   
     |