Step | Hyp | Ref
| Expression |
1 | | f1cocnv1 5491 |
. . . 4
       
   |
2 | | coeq2 4785 |
. . . . 5
  
      |
3 | 2 | eqeq1d 2186 |
. . . 4
    
  
     |
4 | 1, 3 | syl5ibcom 155 |
. . 3
        
    |
5 | 4 | adantr 276 |
. 2
          

       |
6 | | f1fn 5423 |
. . . . . . 7
    
  |
7 | 6 | adantl 277 |
. . . . . 6
          
  |
8 | 7 | adantr 276 |
. . . . 5
                
  |
9 | | f1fn 5423 |
. . . . . . 7
    
  |
10 | 9 | adantr 276 |
. . . . . 6
          
  |
11 | 10 | adantr 276 |
. . . . 5
                
  |
12 | | equid 1701 |
. . . . . . . . . 10
 |
13 | | resieq 4917 |
. . . . . . . . . 10
 
    
   |
14 | 12, 13 | mpbiri 168 |
. . . . . . . . 9
 
      |
15 | 14 | anidms 397 |
. . . . . . . 8
      |
16 | 15 | adantl 277 |
. . . . . . 7
       
      
  
      |
17 | | breq 4005 |
. . . . . . . 8
  
       
      |
18 | 17 | ad2antlr 489 |
. . . . . . 7
       
      
  
             |
19 | 16, 18 | mpbird 167 |
. . . . . 6
       
      
  
        |
20 | | vex 2740 |
. . . . . . . . . 10
 |
21 | 20, 20 | brco 4798 |
. . . . . . . . 9
     
           |
22 | | fnfun 5313 |
. . . . . . . . . . . . . . . . 17
   |
23 | 7, 22 | syl 14 |
. . . . . . . . . . . . . . . 16
          
  |
24 | 23 | adantr 276 |
. . . . . . . . . . . . . . 15
               |
25 | | fndm 5315 |
. . . . . . . . . . . . . . . . . 18
   |
26 | 7, 25 | syl 14 |
. . . . . . . . . . . . . . . . 17
          
  |
27 | 26 | eleq2d 2247 |
. . . . . . . . . . . . . . . 16
          

   |
28 | 27 | biimpar 297 |
. . . . . . . . . . . . . . 15
               |
29 | | funopfvb 5559 |
. . . . . . . . . . . . . . 15
              |
30 | 24, 28, 29 | syl2anc 411 |
. . . . . . . . . . . . . 14
                 
  
   |
31 | 30 | bicomd 141 |
. . . . . . . . . . . . 13
                
       |
32 | | df-br 4004 |
. . . . . . . . . . . . 13
  
  
  |
33 | | eqcom 2179 |
. . . . . . . . . . . . 13
    
      |
34 | 31, 32, 33 | 3bitr4g 223 |
. . . . . . . . . . . 12
               
       |
35 | 34 | biimpd 144 |
. . . . . . . . . . 11
                       |
36 | | df-br 4004 |
. . . . . . . . . . . . . 14
  
  
  |
37 | | fnfun 5313 |
. . . . . . . . . . . . . . . . 17
   |
38 | 10, 37 | syl 14 |
. . . . . . . . . . . . . . . 16
          
  |
39 | 38 | adantr 276 |
. . . . . . . . . . . . . . 15
               |
40 | | fndm 5315 |
. . . . . . . . . . . . . . . . . 18
   |
41 | 10, 40 | syl 14 |
. . . . . . . . . . . . . . . . 17
          
  |
42 | 41 | eleq2d 2247 |
. . . . . . . . . . . . . . . 16
          

   |
43 | 42 | biimpar 297 |
. . . . . . . . . . . . . . 15
               |
44 | | funopfvb 5559 |
. . . . . . . . . . . . . . 15
              |
45 | 39, 43, 44 | syl2anc 411 |
. . . . . . . . . . . . . 14
                 
  
   |
46 | 36, 45 | bitr4id 199 |
. . . . . . . . . . . . 13
               
       |
47 | | vex 2740 |
. . . . . . . . . . . . . 14
 |
48 | 47, 20 | brcnv 4810 |
. . . . . . . . . . . . 13
   
    |
49 | | eqcom 2179 |
. . . . . . . . . . . . 13
    
      |
50 | 46, 48, 49 | 3bitr4g 223 |
. . . . . . . . . . . 12
                        |
51 | 50 | biimpd 144 |
. . . . . . . . . . 11
                        |
52 | 35, 51 | anim12d 335 |
. . . . . . . . . 10
                         
        |
53 | 52 | eximdv 1880 |
. . . . . . . . 9
                             
        |
54 | 21, 53 | biimtrid 152 |
. . . . . . . 8
                         
        |
55 | 6 | anim1i 340 |
. . . . . . . . . 10
     


   |
56 | 55 | adantll 476 |
. . . . . . . . 9
             
   |
57 | | funfvex 5532 |
. . . . . . . . . 10
         |
58 | 57 | funfni 5316 |
. . . . . . . . 9
 
       |
59 | | eqvincg 2861 |
. . . . . . . . 9
             
               |
60 | 56, 58, 59 | 3syl 17 |
. . . . . . . 8
                     
               |
61 | 54, 60 | sylibrd 169 |
. . . . . . 7
                              |
62 | 61 | adantlr 477 |
. . . . . 6
       
      
  
      
           |
63 | 19, 62 | mpd 13 |
. . . . 5
       
      
  
           |
64 | 8, 11, 63 | eqfnfvd 5616 |
. . . 4
                
  |
65 | 64 | eqcomd 2183 |
. . 3
                
  |
66 | 65 | ex 115 |
. 2
          
  
     |
67 | 5, 66 | impbid 129 |
1
          

  
    |