Step | Hyp | Ref
| Expression |
1 | | dfima2 4973 |
. 2
                             |
2 | | elin 3319 |
. . . 4
             

              |
3 | | isof1o 5808 |
. . . . . . . . 9
           |
4 | | f1ofo 5469 |
. . . . . . . . 9
    
      |
5 | | forn 5442 |
. . . . . . . . . 10
       |
6 | 5 | eleq2d 2247 |
. . . . . . . . 9
         |
7 | 3, 4, 6 | 3syl 17 |
. . . . . . . 8
     
   |
8 | | f1ofn 5463 |
. . . . . . . . 9
    
  |
9 | | fvelrnb 5564 |
. . . . . . . . 9
          |
10 | 3, 8, 9 | 3syl 17 |
. . . . . . . 8
     
        |
11 | 7, 10 | bitr3d 190 |
. . . . . . 7
              |
12 | 11 | adantr 276 |
. . . . . 6
 
     

       |
13 | 3, 8 | syl 14 |
. . . . . . . 8
       |
14 | 13 | anim1i 340 |
. . . . . . 7
 
     
   |
15 | | funfvex 5533 |
. . . . . . . 8
         |
16 | 15 | funfni 5317 |
. . . . . . 7
 
       |
17 | | vex 2741 |
. . . . . . . 8
 |
18 | 17 | eliniseg 4999 |
. . . . . . 7
                
         |
19 | 14, 16, 18 | 3syl 17 |
. . . . . 6
 
                
         |
20 | 12, 19 | anbi12d 473 |
. . . . 5
 
      
           
 
   
          |
21 | | elin 3319 |
. . . . . . . . . . . 12
         

          |
22 | | vex 2741 |
. . . . . . . . . . . . . 14
 |
23 | 22 | eliniseg 4999 |
. . . . . . . . . . . . 13
        
     |
24 | 23 | anbi2d 464 |
. . . . . . . . . . . 12
  
       

      |
25 | 21, 24 | bitrid 192 |
. . . . . . . . . . 11
                  |
26 | 25 | anbi1d 465 |
. . . . . . . . . 10
              
           |
27 | | anass 401 |
. . . . . . . . . 10
                   |
28 | 26, 27 | bitrdi 196 |
. . . . . . . . 9
              

          |
29 | 28 | adantl 277 |
. . . . . . . 8
 
                  

          |
30 | | isorel 5809 |
. . . . . . . . . . . . . 14
 
    
 
  
             |
31 | | fnbrfvb 5557 |
. . . . . . . . . . . . . . . . 17
 
           |
32 | 31 | bicomd 141 |
. . . . . . . . . . . . . . . 16
 
           |
33 | 13, 32 | sylan 283 |
. . . . . . . . . . . . . . 15
 
       
       |
34 | 33 | adantrr 479 |
. . . . . . . . . . . . . 14
 
    
 
  
       |
35 | 30, 34 | anbi12d 473 |
. . . . . . . . . . . . 13
 
    
 
      
                   |
36 | | ancom 266 |
. . . . . . . . . . . . . 14
                
    
             |
37 | | breq1 4007 |
. . . . . . . . . . . . . . 15
               
         |
38 | 37 | pm5.32i 454 |
. . . . . . . . . . . . . 14
                
    
         |
39 | 36, 38 | bitri 184 |
. . . . . . . . . . . . 13
                
    
         |
40 | 35, 39 | bitrdi 196 |
. . . . . . . . . . . 12
 
    
 
      
    
          |
41 | 40 | exp32 365 |
. . . . . . . . . . 11
     

      
    
            |
42 | 41 | com23 78 |
. . . . . . . . . 10
     

      
    
            |
43 | 42 | imp 124 |
. . . . . . . . 9
 
            
    
           |
44 | 43 | pm5.32d 450 |
. . . . . . . 8
 
             

                |
45 | 29, 44 | bitrd 188 |
. . . . . . 7
 
                  

                |
46 | 45 | rexbidv2 2480 |
. . . . . 6
 
      
            
               |
47 | | r19.41v 2633 |
. . . . . 6
             
 
   
         |
48 | 46, 47 | bitrdi 196 |
. . . . 5
 
      
                            |
49 | 20, 48 | bitr4d 191 |
. . . 4
 
      
           
                |
50 | 2, 49 | bitrid 192 |
. . 3
 
                                   |
51 | 50 | abbi2dv 2296 |
. 2
 
                                   |
52 | 1, 51 | eqtr4id 2229 |
1
 
                                 |