Proof of Theorem grothprim
Step | Hyp | Ref
| Expression |
1 | | axgroth4 9283 |
. 2
       
             |
2 | | 3anass 995 |
. . . 4
   
              

 

                  |
3 | | dfss2 3433 |
. . . . . . . . . . . . 13

      |
4 | | elin 3629 |
. . . . . . . . . . . . 13
  

   |
5 | 3, 4 | imbi12i 332 |
. . . . . . . . . . . 12
 
  
   
 
    |
6 | 5 | albii 1702 |
. . . . . . . . . . 11
            
 
    |
7 | 6 | rexbii 2901 |
. . . . . . . . . 10
              
 
    |
8 | | df-rex 2755 |
. . . . . . . . . 10
           
          
     |
9 | 7, 8 | bitri 257 |
. . . . . . . . 9
                        |
10 | 9 | ralbii 2831 |
. . . . . . . 8
 

                       |
11 | | df-ral 2754 |
. . . . . . . 8
 
        
    
                    |
12 | 10, 11 | bitri 257 |
. . . . . . 7
 

                   
      |
13 | | dfss2 3433 |
. . . . . . . . . . 11

      |
14 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
15 | | difexg 4565 |
. . . . . . . . . . . . . . 15
 
   |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
   |
17 | | vex 3060 |
. . . . . . . . . . . . . 14
 |
18 | | incom 3637 |
. . . . . . . . . . . . . . 15
     
   |
19 | | disjdif 3851 |
. . . . . . . . . . . . . . 15
     |
20 | 18, 19 | eqtri 2484 |
. . . . . . . . . . . . . 14
     |
21 | 16, 17, 20 | brdom6disj 8986 |
. . . . . . . . . . . . 13
      
    
           |
22 | 21 | orbi1i 527 |
. . . . . . . . . . . 12
    
    
    
            |
23 | | 19.44v 1839 |
. . . . . . . . . . . 12
     
    
                                |
24 | 22, 23 | bitr4i 260 |
. . . . . . . . . . 11
    
    
    
            |
25 | 13, 24 | imbi12i 332 |
. . . . . . . . . 10
 
    
   
     
    
             |
26 | | 19.35 1751 |
. . . . . . . . . 10
             
          
   
     
    
             |
27 | 25, 26 | bitr4i 260 |
. . . . . . . . 9
 
    
   
        
             |
28 | | grothprimlem 9284 |
. . . . . . . . . . . . . . . . . 18
   
            |
29 | 28 | mobii 2333 |
. . . . . . . . . . . . . . . . 17
                    |
30 | | mo2v 2317 |
. . . . . . . . . . . . . . . . 17
                               |
31 | 29, 30 | bitri 257 |
. . . . . . . . . . . . . . . 16
                        |
32 | 31 | ralbii 2831 |
. . . . . . . . . . . . . . 15
 
    

          

      |
33 | | df-ral 2754 |
. . . . . . . . . . . . . . 15
 
              
   
          

       |
34 | 32, 33 | bitri 257 |
. . . . . . . . . . . . . 14
 
    
                      |
35 | | df-ral 2754 |
. . . . . . . . . . . . . . 15
 
      
            |
36 | | eldif 3426 |
. . . . . . . . . . . . . . . . . 18
  

   |
37 | | grothprimlem 9284 |
. . . . . . . . . . . . . . . . . . . 20
   
     

     |
38 | 37 | rexbii 2901 |
. . . . . . . . . . . . . . . . . . 19
    

     

     |
39 | | df-rex 2755 |
. . . . . . . . . . . . . . . . . . 19
           
                |
40 | 38, 39 | bitri 257 |
. . . . . . . . . . . . . . . . . 18
    
                |
41 | 36, 40 | imbi12i 332 |
. . . . . . . . . . . . . . . . 17
    
                        |
42 | | pm5.6 928 |
. . . . . . . . . . . . . . . . 17
                  

         

        |
43 | 41, 42 | bitri 257 |
. . . . . . . . . . . . . . . 16
    
                        |
44 | 43 | albii 1702 |
. . . . . . . . . . . . . . 15
     

   
                      |
45 | 35, 44 | bitri 257 |
. . . . . . . . . . . . . 14
 
      
                      |
46 | 34, 45 | anbi12i 708 |
. . . . . . . . . . . . 13
                                        

                   |
47 | | 19.26 1743 |
. . . . . . . . . . . . 13
               

                       
   
          

       

                   |
48 | 46, 47 | bitr4i 260 |
. . . . . . . . . . . 12
                                                           |
49 | 48 | orbi1i 527 |
. . . . . . . . . . 11
        
         
               

                           |
50 | 49 | imbi2i 318 |
. . . . . . . . . 10
   
  
               
 
                                              |
51 | 50 | exbii 1729 |
. . . . . . . . 9
             
          
   
                

                            |
52 | 27, 51 | bitri 257 |
. . . . . . . 8
 
    
   
                

                            |
53 | 52 | albii 1702 |
. . . . . . 7
        
                      

                            |
54 | 12, 53 | anbi12i 708 |
. . . . . 6
                  
   
          
          
               

                             |
55 | | 19.26 1743 |
. . . . . 6
               
                        

                          
   
          
          
               

                             |
56 | 54, 55 | bitr4i 260 |
. . . . 5
                  
   
          
                        

                             |
57 | 56 | anbi2i 705 |
. . . 4
                                            
                

                              |
58 | 2, 57 | bitri 257 |
. . 3
   
              

   
          
                        

                              |
59 | 58 | exbii 1729 |
. 2
    

        
            
          
                        

                              |
60 | 1, 59 | mpbi 213 |
1
                         
                

                             |