Step | Hyp | Ref
| Expression |
1 | | elin 3120 |
. . . 4
                             |
2 | | isof1o 5390 |
. . . . . . . . 9
           |
3 | | f1ofo 5076 |
. . . . . . . . 9
           |
4 | | forn 5052 |
. . . . . . . . . 10
       |
5 | 4 | eleq2d 2104 |
. . . . . . . . 9
     
   |
6 | 2, 3, 5 | 3syl 17 |
. . . . . . . 8
         |
7 | | f1ofn 5070 |
. . . . . . . . 9
       |
8 | | fvelrnb 5164 |
. . . . . . . . 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 5135 |
. . . . . . . 8
         |
15 | 14 | funfni 4942 |
. . . . . . 7
 
    
  |
16 | | vex 2554 |
. . . . . . . 8
 |
17 | 16 | eliniseg 4638 |
. . . . . . 7
     
                    |
18 | 13, 15, 17 | 3syl 17 |
. . . . . 6
 
                          |
19 | 11, 18 | anbi12d 442 |
. . . . 5
 
                        
          |
20 | | elin 3120 |
. . . . . . . . . . . 12
                     |
21 | | vex 2554 |
. . . . . . . . . . . . . 14
 |
22 | 21 | eliniseg 4638 |
. . . . . . . . . . . . 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 5391 |
. . . . . . . . . . . . . 14
 
                       |
30 | | fnbrfvb 5157 |
. . . . . . . . . . . . . . . . 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 3758 |
. . . . . . . . . . . . . . 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 2323 |
. . . . . 6
 
                                   |
46 | | r19.41v 2460 |
. . . . . 6
 
             
   
         |
47 | 45, 46 | syl6bb 185 |
. . . . 5
 
                    
   
          |
48 | 19, 47 | bitr4d 180 |
. . . 4
 
                                   |
49 | 1, 48 | syl5bb 181 |
. . 3
 
                                   |
50 | 49 | abbi2dv 2153 |
. 2
 
                   
               |
51 | | dfima2 4613 |
. 2
              
              |
52 | 50, 51 | syl6reqr 2088 |
1
 
        
                        |