Step | Hyp | Ref
| Expression |
1 | | df-enq0 7037 |
. . 3
~Q0        
                            |
2 | | df-xp 4457 |
. . 3
                  |
3 | 1, 2 | ineq12i 3200 |
. 2
~Q0
               
                                        |
4 | | inopab 4581 |
. 2
        
                                          
    
                            
      |
5 | | an32 530 |
. . . . . 6
        
                         
   
    
                                   |
6 | | an4 554 |
. . . . . . . 8
    
         
                |
7 | | pinn 6922 |
. . . . . . . . . . . . 13
   |
8 | 7 | ssriv 3030 |
. . . . . . . . . . . 12
 |
9 | | xpss1 4561 |
. . . . . . . . . . . 12

      |
10 | 8, 9 | ax-mp 7 |
. . . . . . . . . . 11
     |
11 | 10 | sseli 3022 |
. . . . . . . . . 10
  
    |
12 | 11 | pm4.71ri 385 |
. . . . . . . . 9
  
        |
13 | 10 | sseli 3022 |
. . . . . . . . . 10
  
    |
14 | 13 | pm4.71ri 385 |
. . . . . . . . 9
  
        |
15 | 12, 14 | anbi12i 449 |
. . . . . . . 8
      
                |
16 | 6, 15 | bitr4i 186 |
. . . . . . 7
    
         
        |
17 | 16 | anbi1i 447 |
. . . . . 6
        
                                 
                            |
18 | 5, 17 | bitri 183 |
. . . . 5
        
                         
   
                                |
19 | | eleq1 2151 |
. . . . . . . . . . . . . . . . . . 19
               |
20 | | opelxp 4480 |
. . . . . . . . . . . . . . . . . . 19
          |
21 | 19, 20 | syl6bb 195 |
. . . . . . . . . . . . . . . . . 18
            |
22 | | eleq1 2151 |
. . . . . . . . . . . . . . . . . . 19
               |
23 | | opelxp 4480 |
. . . . . . . . . . . . . . . . . . 19
          |
24 | 22, 23 | syl6bb 195 |
. . . . . . . . . . . . . . . . . 18
            |
25 | 21, 24 | bi2anan9 574 |
. . . . . . . . . . . . . . . . 17
    
   
      
 
       |
26 | 25 | pm5.32i 443 |
. . . . . . . . . . . . . . . 16
            
   
    
     
       |
27 | 26 | anbi1i 447 |
. . . . . . . . . . . . . . 15
                                  


          |
28 | | anass 394 |
. . . . . . . . . . . . . . 15
                      
    
          
        |
29 | 27, 28 | bitri 183 |
. . . . . . . . . . . . . 14
                                  


 
        |
30 | | mulpiord 6930 |
. . . . . . . . . . . . . . . . . 18
 
       |
31 | | mulpiord 6930 |
. . . . . . . . . . . . . . . . . 18
 
       |
32 | 30, 31 | eqeqan12d 2104 |
. . . . . . . . . . . . . . . . 17
      
    
       |
33 | 32 | an42s 557 |
. . . . . . . . . . . . . . . 16
      
    
       |
34 | 33 | pm5.32i 443 |
. . . . . . . . . . . . . . 15
   


 
       
   
       |
35 | 34 | anbi2i 446 |
. . . . . . . . . . . . . 14
                
     
    
          
        |
36 | 29, 35 | bitr4i 186 |
. . . . . . . . . . . . 13
                                  


 
        |
37 | | anass 394 |
. . . . . . . . . . . . 13
                      
    
          
        |
38 | 36, 37 | bitr4i 186 |
. . . . . . . . . . . 12
                                  


          |
39 | 26 | anbi1i 447 |
. . . . . . . . . . . 12
                                  


          |
40 | 38, 39 | bitr4i 186 |
. . . . . . . . . . 11
                                   
           |
41 | | ancom 263 |
. . . . . . . . . . . 12
            
   
          
       |
42 | 41 | anbi1i 447 |
. . . . . . . . . . 11
                           
      
            |
43 | 41 | anbi1i 447 |
. . . . . . . . . . 11
                           
      
            |
44 | 40, 42, 43 | 3bitr3i 209 |
. . . . . . . . . 10
        
        
                
            |
45 | | anass 394 |
. . . . . . . . . 10
        
        
        
                    |
46 | | anass 394 |
. . . . . . . . . 10
        
        
        
                    |
47 | 44, 45, 46 | 3bitr3i 209 |
. . . . . . . . 9
    
                     
                    |
48 | 47 | 2exbii 1543 |
. . . . . . . 8
        
                            
    
            |
49 | | 19.42vv 1837 |
. . . . . . . 8
        
                     
           
            |
50 | | 19.42vv 1837 |
. . . . . . . 8
        
                     
           
            |
51 | 48, 49, 50 | 3bitr3i 209 |
. . . . . . 7
    
                         
           
            |
52 | 51 | 2exbii 1543 |
. . . . . 6
        
                                
                     |
53 | | 19.42vv 1837 |
. . . . . 6
        
                         
                            |
54 | | 19.42vv 1837 |
. . . . . 6
        
                         
                            |
55 | 52, 53, 54 | 3bitr3i 209 |
. . . . 5
    
                             
                            |
56 | 18, 55 | bitri 183 |
. . . 4
        
                         
   
                                |
57 | 56 | opabbii 3911 |
. . 3
           
                         
            
                            |
58 | | df-enq 6960 |
. . 3
   
                                |
59 | 57, 58 | eqtr4i 2112 |
. 2
           
                         
      |
60 | 3, 4, 59 | 3eqtrri 2114 |
1
~Q0   
     |