Step | Hyp | Ref
| Expression |
1 | | elin 3126 |
. . . 4
             

              |
2 | | isof1o 5447 |
. . . . . . . . 9
           |
3 | | f1ofo 5133 |
. . . . . . . . 9
    
      |
4 | | forn 5109 |
. . . . . . . . . 10
       |
5 | 4 | eleq2d 2107 |
. . . . . . . . 9
         |
6 | 2, 3, 5 | 3syl 17 |
. . . . . . . 8
     
   |
7 | | f1ofn 5127 |
. . . . . . . . 9
    
  |
8 | | fvelrnb 5221 |
. . . . . . . . 9
          |
9 | 2, 7, 8 | 3syl 17 |
. . . . . . . 8
     
        |
10 | 6, 9 | bitr3d 179 |
. . . . . . 7
              |
11 | 10 | adantr 261 |
. . . . . 6
 
     

       |
12 | 2, 7 | syl 14 |
. . . . . . . 8
       |
13 | 12 | anim1i 323 |
. . . . . . 7
 
     
   |
14 | | funfvex 5192 |
. . . . . . . 8
         |
15 | 14 | funfni 4999 |
. . . . . . 7
 
       |
16 | | vex 2560 |
. . . . . . . 8
 |
17 | 16 | eliniseg 4695 |
. . . . . . 7
                
         |
18 | 13, 15, 17 | 3syl 17 |
. . . . . 6
 
                
         |
19 | 11, 18 | anbi12d 442 |
. . . . 5
 
      
           
 
   
          |
20 | | elin 3126 |
. . . . . . . . . . . 12
         

          |
21 | | vex 2560 |
. . . . . . . . . . . . . 14
 |
22 | 21 | eliniseg 4695 |
. . . . . . . . . . . . 13
        
     |
23 | 22 | anbi2d 437 |
. . . . . . . . . . . 12
  
       

      |
24 | 20, 23 | syl5bb 181 |
. . . . . . . . . . 11
                  |
25 | 24 | anbi1d 438 |
. . . . . . . . . 10
              
           |
26 | | anass 381 |
. . . . . . . . . 10
                   |
27 | 25, 26 | syl6bb 185 |
. . . . . . . . 9
              

          |
28 | 27 | adantl 262 |
. . . . . . . 8
 
                  

          |
29 | | isorel 5448 |
. . . . . . . . . . . . . 14
 
    
 
  
             |
30 | | fnbrfvb 5214 |
. . . . . . . . . . . . . . . . 17
 
           |
31 | 30 | bicomd 129 |
. . . . . . . . . . . . . . . 16
 
           |
32 | 12, 31 | sylan 267 |
. . . . . . . . . . . . . . 15
 
       
       |
33 | 32 | adantrr 448 |
. . . . . . . . . . . . . 14
 
    
 
  
       |
34 | 29, 33 | anbi12d 442 |
. . . . . . . . . . . . 13
 
    
 
      
                   |
35 | | ancom 253 |
. . . . . . . . . . . . . 14
                
    
             |
36 | | breq1 3767 |
. . . . . . . . . . . . . . 15
               
         |
37 | 36 | pm5.32i 427 |
. . . . . . . . . . . . . 14
                
    
         |
38 | 35, 37 | bitri 173 |
. . . . . . . . . . . . 13
                
    
         |
39 | 34, 38 | syl6bb 185 |
. . . . . . . . . . . 12
 
    
 
      
    
          |
40 | 39 | exp32 347 |
. . . . . . . . . . 11
     

      
    
            |
41 | 40 | com23 72 |
. . . . . . . . . 10
     

      
    
            |
42 | 41 | imp 115 |
. . . . . . . . 9
 
            
    
           |
43 | 42 | pm5.32d 423 |
. . . . . . . 8
 
             

                |
44 | 28, 43 | bitrd 177 |
. . . . . . 7
 
                  

                |
45 | 44 | rexbidv2 2329 |
. . . . . 6
 
      
            
               |
46 | | r19.41v 2466 |
. . . . . 6
             
 
   
         |
47 | 45, 46 | syl6bb 185 |
. . . . 5
 
      
                            |
48 | 19, 47 | bitr4d 180 |
. . . 4
 
      
           
                |
49 | 1, 48 | syl5bb 181 |
. . 3
 
                                   |
50 | 49 | abbi2dv 2156 |
. 2
 
                                   |
51 | | dfima2 4670 |
. 2
                             |
52 | 50, 51 | syl6reqr 2091 |
1
 
                                 |