Step | Hyp | Ref
| Expression |
1 | | dff12 5034 |
. 2
                  |
2 | | ffn 4989 |
. . . 4
       |
3 | | vex 2554 |
. . . . . . . . . . . . . . 15
 |
4 | | vex 2554 |
. . . . . . . . . . . . . . 15
 |
5 | 3, 4 | breldm 4482 |
. . . . . . . . . . . . . 14
     |
6 | | fndm 4941 |
. . . . . . . . . . . . . . 15
   |
7 | 6 | eleq2d 2104 |
. . . . . . . . . . . . . 14
 
   |
8 | 5, 7 | syl5ib 143 |
. . . . . . . . . . . . 13
       |
9 | | vex 2554 |
. . . . . . . . . . . . . . 15
 |
10 | 9, 4 | breldm 4482 |
. . . . . . . . . . . . . 14
     |
11 | 6 | eleq2d 2104 |
. . . . . . . . . . . . . 14
 
   |
12 | 10, 11 | syl5ib 143 |
. . . . . . . . . . . . 13
       |
13 | 8, 12 | anim12d 318 |
. . . . . . . . . . . 12
        
    |
14 | 13 | pm4.71rd 374 |
. . . . . . . . . . 11
         
           |
15 | | eqcom 2039 |
. . . . . . . . . . . . . . 15
    
      |
16 | | fnbrfvb 5157 |
. . . . . . . . . . . . . . 15
 
     
     |
17 | 15, 16 | syl5bb 181 |
. . . . . . . . . . . . . 14
 
           |
18 | | eqcom 2039 |
. . . . . . . . . . . . . . 15
    
      |
19 | | fnbrfvb 5157 |
. . . . . . . . . . . . . . 15
 
     
     |
20 | 18, 19 | syl5bb 181 |
. . . . . . . . . . . . . 14
 
           |
21 | 17, 20 | bi2anan9 538 |
. . . . . . . . . . . . 13
  
   
 
   
              |
22 | 21 | anandis 526 |
. . . . . . . . . . . 12
  
 
 
   
              |
23 | 22 | pm5.32da 425 |
. . . . . . . . . . 11
   
             
           |
24 | 14, 23 | bitr4d 180 |
. . . . . . . . . 10
         
     
         |
25 | 24 | imbi1d 220 |
. . . . . . . . 9
              
              |
26 | | impexp 250 |
. . . . . . . . 9
     
            
                |
27 | 25, 26 | syl6bb 185 |
. . . . . . . 8
              
   
          |
28 | 27 | albidv 1702 |
. . . . . . 7
          
       
   
          |
29 | | 19.21v 1750 |
. . . . . . . 8
       
   
        
        
    
    |
30 | | funfvex 5135 |
. . . . . . . . . . . . . 14
         |
31 | 30 | funfni 4942 |
. . . . . . . . . . . . 13
 
    
  |
32 | | eqvincg 2662 |
. . . . . . . . . . . . 13
             
  
   
        |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . 12
 
     
                   |
34 | 33 | imbi1d 220 |
. . . . . . . . . . 11
 
               
   
         |
35 | | 19.23v 1760 |
. . . . . . . . . . 11
                      
        |
36 | 34, 35 | syl6rbbr 188 |
. . . . . . . . . 10
 
         
                   |
37 | 36 | adantrr 448 |
. . . . . . . . 9
  
 
        
    
         
    |
38 | 37 | pm5.74da 417 |
. . . . . . . 8
   
        
        
     
         |
39 | 29, 38 | syl5bb 181 |
. . . . . . 7
        
   
        
     
         |
40 | 28, 39 | bitrd 177 |
. . . . . 6
          
  
               |
41 | 40 | 2albidv 1744 |
. . . . 5
                               
     |
42 | | breq1 3758 |
. . . . . . . 8
         |
43 | 42 | mo4 1958 |
. . . . . . 7
                  |
44 | 43 | albii 1356 |
. . . . . 6
                  
   |
45 | | alrot3 1371 |
. . . . . 6
                               |
46 | 44, 45 | bitri 173 |
. . . . 5
                  
   |
47 | | r2al 2337 |
. . . . 5
 
                          
    |
48 | 41, 46, 47 | 3bitr4g 212 |
. . . 4
                      |
49 | 2, 48 | syl 14 |
. . 3
                          |
50 | 49 | pm5.32i 427 |
. 2
                  
        
    |
51 | 1, 50 | bitri 173 |
1
           
        
    |