Step | Hyp | Ref
| Expression |
1 | | vex 3057 |
. . 3
 |
2 | 1 | eldm2 5122 |
. 2

       |
3 | | frrlem10.4 |
. . . . . . 7
  |
4 | | frrlem10.3 |
. . . . . . . 8
     
                         |
5 | 4 | unieqi 4184 |
. . . . . . 7
      
                          |
6 | 3, 5 | eqtri 2478 |
. . . . . 6
     
                          |
7 | 6 | eleq2i 2526 |
. . . . 5
   
        
                           |
8 | | eluniab 4186 |
. . . . 5
         
                                  
                           |
9 | 7, 8 | bitri 249 |
. . . 4
   
     
                      
        |
10 | 4 | abeq2i 2575 |
. . . . . . . 8

                      
       |
11 | | elssuni 4205 |
. . . . . . . . 9
    |
12 | 11, 3 | syl6sseqr 3487 |
. . . . . . . 8
   |
13 | 10, 12 | sylbir 213 |
. . . . . . 7
     
                      
  |
14 | | fnop 5598 |
. . . . . . . . . . . 12
        |
15 | 14 | ex 434 |
. . . . . . . . . . 11
    
   |
16 | | rsp 2862 |
. . . . . . . . . . . . . . . . . . . 20
 
          
    
           
      |
17 | 16 | impcom 430 |
. . . . . . . . . . . . . . . . . . 19
             
    
           
     |
18 | | rsp 2862 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         
    |
19 | | fndm 5594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  |
20 | | sseq2 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     

    
   |
21 | | eleq2 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
22 | 20, 21 | anbi12d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
  
     
    |
23 | 19, 22 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
 
     
    |
24 | 23 | biimprd 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
       
    |
25 | 24 | expd 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
           |
26 | 25 | impcom 430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       
     |
27 | | frrlem10.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
28 | | frrlem10.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Se  |
29 | 27, 28, 4, 3 | frrlem10 27899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
30 | | funssfv 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
31 | 30 | 3adant3l 1215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
            |
32 | | fun2ssres 5543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
       
      
    |
33 | 32 | 3adant3r 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
                  |
34 | 33 | oveq2d 6192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
        
          
      |
35 | 31, 34 | eqeq12d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
          
      
           
      |
36 | 35 | biimprd 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
          
                         |
37 | 29, 36 | mp3an1 1302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
    
           
                         |
38 | 37 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
               
             
        |
39 | 38 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
              
   
          
        |
40 | 26, 39 | syl6com 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
                 

           
        |
41 | 40 | expd 436 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
           
                
         |
42 | 41 | com34 83 |
. . . . . . . . . . . . . . . . . . . . . 22
               
                              |
43 | 18, 42 | sylcom 29 |
. . . . . . . . . . . . . . . . . . . . 21
 
                  
                          |
44 | 43 | adantl 466 |
. . . . . . . . . . . . . . . . . . . 20
 
      

           
    

           
         |
45 | 44 | com14 88 |
. . . . . . . . . . . . . . . . . . 19
              
            
          
          |
46 | 17, 45 | syl7 68 |
. . . . . . . . . . . . . . . . . 18
    
           
          
  
          
          |
47 | 46 | exp4a 606 |
. . . . . . . . . . . . . . . . 17
                
            
          
           |
48 | 47 | pm2.43d 48 |
. . . . . . . . . . . . . . . 16
               
            
          
          |
49 | 48 | com34 83 |
. . . . . . . . . . . . . . 15
        
   
              

           
         |
50 | 49 | imp 429 |
. . . . . . . . . . . . . 14
 
       
   
              

           
        |
51 | 50 | expd 436 |
. . . . . . . . . . . . 13
 
       

 
          
                
         |
52 | 51 | 3impd 1202 |
. . . . . . . . . . . 12
 
       
 
           
                        |
53 | 52 | ex 434 |
. . . . . . . . . . 11
        
 
           
                         |
54 | 15, 53 | syld 44 |
. . . . . . . . . 10
    
 
                       
          
         |
55 | 54 | com12 31 |
. . . . . . . . 9
   
                     
                         |
56 | 55 | impd 431 |
. . . . . . . 8
   
  
                                            |
57 | 56 | exlimdv 1691 |
. . . . . . 7
   
     
                                           |
58 | 13, 57 | mpdi 42 |
. . . . . 6
   
     
                                         |
59 | 58 | imp 429 |
. . . . 5
    
                      
     
           
     |
60 | 59 | exlimiv 1689 |
. . . 4
          
                                    
     |
61 | 9, 60 | sylbi 195 |
. . 3
   
       
         |
62 | 61 | exlimiv 1689 |
. 2
                
      |
63 | 2, 62 | sylbi 195 |
1
                  |