Step | Hyp | Ref
| Expression |
1 | | xpcomf1o.1 |
. . . . . . . . . 10
         |
2 | 1 | xpcomf1o 7658 |
. . . . . . . . 9
      
  |
3 | | f1ofun 5814 |
. . . . . . . . 9
        
  |
4 | | funbrfv2b 5907 |
. . . . . . . . 9

  

        |
5 | 2, 3, 4 | mp2b 10 |
. . . . . . . 8
  
        |
6 | | ancom 452 |
. . . . . . . 8
               |
7 | | eqcom 2457 |
. . . . . . . . 9
    
      |
8 | | f1odm 5816 |
. . . . . . . . . . 11
        
    |
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . 10
   |
10 | 9 | eleq2i 2520 |
. . . . . . . . 9


   |
11 | 7, 10 | anbi12i 702 |
. . . . . . . 8
     
           |
12 | 5, 6, 11 | 3bitri 275 |
. . . . . . 7
  
          |
13 | 12 | anbi1i 700 |
. . . . . 6
      
     
        |
14 | | anass 654 |
. . . . . 6
            
              |
15 | 13, 14 | bitri 253 |
. . . . 5
      
              |
16 | 15 | exbii 1717 |
. . . 4
        
         
      |
17 | | fvex 5873 |
. . . . 5
     |
18 | | breq1 4404 |
. . . . . 6
       
         |
19 | 18 | anbi2d 709 |
. . . . 5
              
          |
20 | 17, 19 | ceqsexv 3083 |
. . . 4
       
  
   
  
         |
21 | | elxp 4850 |
. . . . . 6
  
        
    |
22 | 21 | anbi1i 700 |
. . . . 5
          
                     |
23 | | nfcv 2591 |
. . . . . . 7
       |
24 | | xpcomco.1 |
. . . . . . . 8
 
  |
25 | | nfmpt22 6356 |
. . . . . . . 8
   
  |
26 | 24, 25 | nfcxfr 2589 |
. . . . . . 7
   |
27 | | nfcv 2591 |
. . . . . . 7
   |
28 | 23, 26, 27 | nfbr 4446 |
. . . . . 6
         |
29 | 28 | 19.41 2050 |
. . . . 5
          
 
                
           |
30 | | nfcv 2591 |
. . . . . . . . 9
       |
31 | | nfmpt21 6355 |
. . . . . . . . . 10
   
  |
32 | 24, 31 | nfcxfr 2589 |
. . . . . . . . 9
   |
33 | | nfcv 2591 |
. . . . . . . . 9
   |
34 | 30, 32, 33 | nfbr 4446 |
. . . . . . . 8
         |
35 | 34 | 19.41 2050 |
. . . . . . 7
                 
       
           |
36 | | anass 654 |
. . . . . . . . 9
      
 
                        |
37 | | fveq2 5863 |
. . . . . . . . . . . . . 14
                 |
38 | | opelxpi 4865 |
. . . . . . . . . . . . . . 15
 
        |
39 | | sneq 3977 |
. . . . . . . . . . . . . . . . . . 19
             |
40 | 39 | cnveqd 5009 |
. . . . . . . . . . . . . . . . . 18
      
        |
41 | 40 | unieqd 4207 |
. . . . . . . . . . . . . . . . 17
       
         |
42 | | opswap 5322 |
. . . . . . . . . . . . . . . . 17
           |
43 | 41, 42 | syl6eq 2500 |
. . . . . . . . . . . . . . . 16
       
     |
44 | | opex 4663 |
. . . . . . . . . . . . . . . 16
    |
45 | 43, 1, 44 | fvmpt 5946 |
. . . . . . . . . . . . . . 15
     
      
     |
46 | 38, 45 | syl 17 |
. . . . . . . . . . . . . 14
 
             |
47 | 37, 46 | sylan9eq 2504 |
. . . . . . . . . . . . 13
     
 
         |
48 | 47 | breq1d 4411 |
. . . . . . . . . . . 12
     
 
      
        |
49 | | df-br 4402 |
. . . . . . . . . . . . . . . 16
     
        |
50 | | df-mpt2 6293 |
. . . . . . . . . . . . . . . . . 18
         
 

   |
51 | 24, 50 | eqtri 2472 |
. . . . . . . . . . . . . . . . 17
     
       |
52 | 51 | eleq2i 2520 |
. . . . . . . . . . . . . . . 16
                  
        |
53 | | oprabid 6315 |
. . . . . . . . . . . . . . . 16
            
     
 

   |
54 | 49, 52, 53 | 3bitri 275 |
. . . . . . . . . . . . . . 15
     
 

   |
55 | 54 | baib 913 |
. . . . . . . . . . . . . 14
 
      
   |
56 | 55 | ancoms 455 |
. . . . . . . . . . . . 13
 
      
   |
57 | 56 | adantl 468 |
. . . . . . . . . . . 12
     
 
         |
58 | 48, 57 | bitrd 257 |
. . . . . . . . . . 11
     
 
      
   |
59 | 58 | pm5.32da 646 |
. . . . . . . . . 10
      
               |
60 | 59 | pm5.32i 642 |
. . . . . . . . 9
      

       
           |
61 | 36, 60 | bitri 253 |
. . . . . . . 8
      
 
                  |
62 | 61 | exbii 1717 |
. . . . . . 7
                 
       

    |
63 | 35, 62 | bitr3i 255 |
. . . . . 6
                 
       

    |
64 | 63 | exbii 1717 |
. . . . 5
          
 
                

    |
65 | 22, 29, 64 | 3bitr2i 277 |
. . . 4
          
               |
66 | 16, 20, 65 | 3bitri 275 |
. . 3
        
               |
67 | 66 | opabbii 4466 |
. 2
                
               |
68 | | df-co 4842 |
. 2
     
          |
69 | | df-mpt2 6293 |
. . 3
         
 

   |
70 | | dfoprab2 6334 |
. . 3
        

     
               |
71 | 69, 70 | eqtri 2472 |
. 2
                      |
72 | 67, 68, 71 | 3eqtr4i 2482 |
1
   
  |