Step | Hyp | Ref
| Expression |
1 | | untelirr 30384 |
. . . . 5
 
   
 
   
 
   
    |
2 | | eluni2 4216 |
. . . . . 6
    
           |
3 | | vex 3060 |
. . . . . . . . . 10
 |
4 | | sseq1 3465 |
. . . . . . . . . . 11
 
   |
5 | | treq 4517 |
. . . . . . . . . . 11
 
   |
6 | | raleq 2999 |
. . . . . . . . . . 11
  

   |
7 | 4, 5, 6 | 3anbi123d 1348 |
. . . . . . . . . 10
   
 

    |
8 | 3, 7 | elab 3197 |
. . . . . . . . 9
   
   
   |
9 | | elequ1 1905 |
. . . . . . . . . . . . . 14
 
   |
10 | | elequ2 1912 |
. . . . . . . . . . . . . 14
 
   |
11 | 9, 10 | bitrd 261 |
. . . . . . . . . . . . 13
 
   |
12 | 11 | notbid 300 |
. . . . . . . . . . . 12
 
   |
13 | 12 | cbvralv 3031 |
. . . . . . . . . . 11
 

  |
14 | 13 | biimpi 199 |
. . . . . . . . . 10
 

  |
15 | 14 | 3ad2ant3 1037 |
. . . . . . . . 9
 

 
  |
16 | 8, 15 | sylbi 200 |
. . . . . . . 8
   
  
  |
17 | | rsp 2766 |
. . . . . . . 8
 

   |
18 | 16, 17 | syl 17 |
. . . . . . 7
   
  
   |
19 | 18 | rexlimiv 2885 |
. . . . . 6
    
     |
20 | 2, 19 | sylbi 200 |
. . . . 5
    
 
  |
21 | 1, 20 | mprg 2763 |
. . . 4
 


    

   |
22 | | dfon2lem2 30479 |
. . . . 5
       |
23 | | dfpss2 3530 |
. . . . . 6
  


      
    

     |
24 | | dfon2lem1 30478 |
. . . . . . 7
 


   |
25 | | ssexg 4563 |
. . . . . . . . . 10
     
           |
26 | 22, 25 | mpan 681 |
. . . . . . . . 9
         |
27 | | psseq1 3532 |
. . . . . . . . . . . . 13
    
      
     |
28 | | treq 4517 |
. . . . . . . . . . . . 13
    
      
     |
29 | 27, 28 | anbi12d 722 |
. . . . . . . . . . . 12
    
    
  


            |
30 | | eleq1 2528 |
. . . . . . . . . . . 12
    
      
 
   |
31 | 29, 30 | imbi12d 326 |
. . . . . . . . . . 11
    
    
 
    

            
 
    |
32 | 31 | spcgv 3146 |
. . . . . . . . . 10
  


        
    

            
 
    |
33 | 32 | imp 435 |
. . . . . . . . 9
     
 
                         
 
   |
34 | 26, 33 | sylan 478 |
. . . . . . . 8
                           
 
   |
35 | | snssi 4129 |
. . . . . . . . . 10
  


            |
36 | | df-suc 5448 |
. . . . . . . . . . . . 13
 


      
 
          |
37 | 36 | sseq1i 3468 |
. . . . . . . . . . . 12
   

      
 
        
  |
38 | | unss 3620 |
. . . . . . . . . . . 12
     
     

   
  


      
      |
39 | 37, 38 | bitr4i 260 |
. . . . . . . . . . 11
   

      
     

      |
40 | 39 | biimpri 211 |
. . . . . . . . . 10
     
     

      

    |
41 | 22, 35, 40 | sylancr 674 |
. . . . . . . . 9
  


 
   
    |
42 | | suctr 5525 |
. . . . . . . . . . . . 13
    
 
        |
43 | 24, 42 | ax-mp 5 |
. . . . . . . . . . . 12
  

   |
44 | | untuni 30385 |
. . . . . . . . . . . . . 14
 
   
  
  
   
  |
45 | 44, 16 | mprgbir 2764 |
. . . . . . . . . . . . 13
    
   |
46 | | nfv 1772 |
. . . . . . . . . . . . . . . . 17

 |
47 | | nfv 1772 |
. . . . . . . . . . . . . . . . 17
   |
48 | | nfra1 2781 |
. . . . . . . . . . . . . . . . 17
  
 |
49 | 46, 47, 48 | nf3an 2024 |
. . . . . . . . . . . . . . . 16
   
  |
50 | 49 | nfab 2607 |
. . . . . . . . . . . . . . 15
  


   |
51 | 50 | nfuni 4218 |
. . . . . . . . . . . . . 14
    

   |
52 | 51 | untsucf 30386 |
. . . . . . . . . . . . 13
 
   
     

 
  |
53 | 45, 52 | ax-mp 5 |
. . . . . . . . . . . 12
    
   |
54 | | sucexg 6664 |
. . . . . . . . . . . . . 14
  


 
   
 
  |
55 | | sseq1 3465 |
. . . . . . . . . . . . . . . . 17
       
         |
56 | | treq 4517 |
. . . . . . . . . . . . . . . . 17
       
 


     |
57 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . 18
   |
58 | 51 | nfsuc 5513 |
. . . . . . . . . . . . . . . . . 18
    
   |
59 | 57, 58 | raleqf 2995 |
. . . . . . . . . . . . . . . . 17
         
  

 
   |
60 | 55, 56, 59 | 3anbi123d 1348 |
. . . . . . . . . . . . . . . 16
         
     
     
      
      |
61 | | sseq1 3465 |
. . . . . . . . . . . . . . . . . 18
 
   |
62 | | treq 4517 |
. . . . . . . . . . . . . . . . . 18
 
   |
63 | | raleq 2999 |
. . . . . . . . . . . . . . . . . 18
  
    |
64 | 61, 62, 63 | 3anbi123d 1348 |
. . . . . . . . . . . . . . . . 17
   
 

    |
65 | 64 | cbvabv 2586 |
. . . . . . . . . . . . . . . 16
  
 
      |
66 | 60, 65 | elab2g 3199 |
. . . . . . . . . . . . . . 15
   

    


      
   

   


    


 
    |
67 | 66 | biimprd 231 |
. . . . . . . . . . . . . 14
   

      

   


    


 
    
 
  
     |
68 | 54, 67 | syl 17 |
. . . . . . . . . . . . 13
  


      

   


    


 
    
 
  
     |
69 | 68 | com12 32 |
. . . . . . . . . . . 12
     
     
      
  
  


 
   
 
  
     |
70 | 43, 53, 69 | mp3an23 1365 |
. . . . . . . . . . 11
   

        
   
 
  
     |
71 | 70 | com12 32 |
. . . . . . . . . 10
  


    


 
   
 
  
     |
72 | | elssuni 4241 |
. . . . . . . . . . 11
   

         

    

    |
73 | | sucssel 5534 |
. . . . . . . . . . 11
  


    


    

    

    

     |
74 | 72, 73 | syl5 33 |
. . . . . . . . . 10
  


    


         

    

     |
75 | 71, 74 | syld 45 |
. . . . . . . . 9
  


    


     
 
   
     |
76 | 41, 75 | mpd 15 |
. . . . . . . 8
  


     
 
   
    |
77 | 34, 76 | syl6 34 |
. . . . . . 7
                           
 
   
     |
78 | 24, 77 | mpan2i 688 |
. . . . . 6
             
          

     |
79 | 23, 78 | syl5bir 226 |
. . . . 5
                                

     |
80 | 22, 79 | mpani 687 |
. . . 4
                   
 
   
     |
81 | 21, 80 | mt3i 131 |
. . 3
           

    |
82 | 24, 45 | pm3.2i 461 |
. . . 4
    
      
    |
83 | | treq 4517 |
. . . . 5
  


    


 
   |
84 | | raleq 2999 |
. . . . 5
  


       
  
   |
85 | 83, 84 | anbi12d 722 |
. . . 4
  


       
      
    
    |
86 | 82, 85 | mpbii 216 |
. . 3
  


   
   |
87 | 81, 86 | syl 17 |
. 2
          
   |
88 | 87 | ex 440 |
1
        

    |