Step | Hyp | Ref
| Expression |
1 | | xpcomf1o.1 |
. . . . . . . . . 10
         |
2 | 1 | xpcomf1o 6595 |
. . . . . . . . 9
      
  |
3 | | f1ofun 5268 |
. . . . . . . . 9
        
  |
4 | | funbrfv2b 5362 |
. . . . . . . . 9

  

        |
5 | 2, 3, 4 | mp2b 8 |
. . . . . . . 8
  
        |
6 | | ancom 263 |
. . . . . . . 8
               |
7 | | eqcom 2091 |
. . . . . . . . 9
    
      |
8 | | f1odm 5270 |
. . . . . . . . . . 11
        
    |
9 | 2, 8 | ax-mp 7 |
. . . . . . . . . 10
   |
10 | 9 | eleq2i 2155 |
. . . . . . . . 9


   |
11 | 7, 10 | anbi12i 449 |
. . . . . . . 8
     
           |
12 | 5, 6, 11 | 3bitri 205 |
. . . . . . 7
  
          |
13 | 12 | anbi1i 447 |
. . . . . 6
      
     
        |
14 | | anass 394 |
. . . . . 6
            
              |
15 | 13, 14 | bitri 183 |
. . . . 5
      
              |
16 | 15 | exbii 1542 |
. . . 4
        
         
      |
17 | | vex 2623 |
. . . . . . 7
 |
18 | 1 | mptfvex 5401 |
. . . . . . 7
               |
19 | 17, 18 | mpan2 417 |
. . . . . 6
      
      |
20 | | vex 2623 |
. . . . . . . . 9
 |
21 | 20 | snex 4026 |
. . . . . . . 8
 
 |
22 | 21 | cnvex 4982 |
. . . . . . 7
    |
23 | 22 | uniex 4273 |
. . . . . 6
     |
24 | 19, 23 | mpg 1386 |
. . . . 5
     |
25 | | breq1 3854 |
. . . . . 6
       
         |
26 | 25 | anbi2d 453 |
. . . . 5
              
          |
27 | 24, 26 | ceqsexv 2659 |
. . . 4
       
  
   
  
         |
28 | | elxp 4469 |
. . . . . 6
  
        
    |
29 | 28 | anbi1i 447 |
. . . . 5
          
                     |
30 | | nfcv 2229 |
. . . . . . 7
       |
31 | | xpcomco.1 |
. . . . . . . 8
 
  |
32 | | nfmpt22 5730 |
. . . . . . . 8
   
  |
33 | 31, 32 | nfcxfr 2226 |
. . . . . . 7
   |
34 | | nfcv 2229 |
. . . . . . 7
   |
35 | 30, 33, 34 | nfbr 3895 |
. . . . . 6
         |
36 | 35 | 19.41 1622 |
. . . . 5
          
 
                
           |
37 | | nfcv 2229 |
. . . . . . . . 9
       |
38 | | nfmpt21 5729 |
. . . . . . . . . 10
   
  |
39 | 31, 38 | nfcxfr 2226 |
. . . . . . . . 9
   |
40 | | nfcv 2229 |
. . . . . . . . 9
   |
41 | 37, 39, 40 | nfbr 3895 |
. . . . . . . 8
         |
42 | 41 | 19.41 1622 |
. . . . . . 7
                 
       
           |
43 | | anass 394 |
. . . . . . . . 9
      
 
                        |
44 | | fveq2 5318 |
. . . . . . . . . . . . . 14
                 |
45 | | opelxpi 4483 |
. . . . . . . . . . . . . . 15
 
        |
46 | | sneq 3461 |
. . . . . . . . . . . . . . . . . . 19
             |
47 | 46 | cnveqd 4625 |
. . . . . . . . . . . . . . . . . 18
      
        |
48 | 47 | unieqd 3670 |
. . . . . . . . . . . . . . . . 17
       
         |
49 | | vex 2623 |
. . . . . . . . . . . . . . . . . 18
 |
50 | | vex 2623 |
. . . . . . . . . . . . . . . . . 18
 |
51 | | opswapg 4930 |
. . . . . . . . . . . . . . . . . 18
 
             |
52 | 49, 50, 51 | mp2an 418 |
. . . . . . . . . . . . . . . . 17
           |
53 | 48, 52 | syl6eq 2137 |
. . . . . . . . . . . . . . . 16
       
     |
54 | 50, 49 | opex 4065 |
. . . . . . . . . . . . . . . 16
    |
55 | 53, 1, 54 | fvmpt 5394 |
. . . . . . . . . . . . . . 15
     
      
     |
56 | 45, 55 | syl 14 |
. . . . . . . . . . . . . 14
 
             |
57 | 44, 56 | sylan9eq 2141 |
. . . . . . . . . . . . 13
     
 
         |
58 | 57 | breq1d 3861 |
. . . . . . . . . . . 12
     
 
      
        |
59 | | df-br 3852 |
. . . . . . . . . . . . . . . 16
     
        |
60 | | df-mpt2 5671 |
. . . . . . . . . . . . . . . . . 18
         
 

   |
61 | 31, 60 | eqtri 2109 |
. . . . . . . . . . . . . . . . 17
     
       |
62 | 61 | eleq2i 2155 |
. . . . . . . . . . . . . . . 16
                  
        |
63 | | oprabid 5695 |
. . . . . . . . . . . . . . . 16
            
     
 

   |
64 | 59, 62, 63 | 3bitri 205 |
. . . . . . . . . . . . . . 15
     
 

   |
65 | 64 | baib 867 |
. . . . . . . . . . . . . 14
 
      
   |
66 | 65 | ancoms 265 |
. . . . . . . . . . . . 13
 
      
   |
67 | 66 | adantl 272 |
. . . . . . . . . . . 12
     
 
         |
68 | 58, 67 | bitrd 187 |
. . . . . . . . . . 11
     
 
      
   |
69 | 68 | pm5.32da 441 |
. . . . . . . . . 10
      
               |
70 | 69 | pm5.32i 443 |
. . . . . . . . 9
      

       
           |
71 | 43, 70 | bitri 183 |
. . . . . . . 8
      
 
                  |
72 | 71 | exbii 1542 |
. . . . . . 7
                 
       

    |
73 | 42, 72 | bitr3i 185 |
. . . . . 6
                 
       

    |
74 | 73 | exbii 1542 |
. . . . 5
          
 
                

    |
75 | 29, 36, 74 | 3bitr2i 207 |
. . . 4
          
               |
76 | 16, 27, 75 | 3bitri 205 |
. . 3
        
               |
77 | 76 | opabbii 3911 |
. 2
                
               |
78 | | df-co 4461 |
. 2
     
          |
79 | | df-mpt2 5671 |
. . 3
         
 

   |
80 | | dfoprab2 5710 |
. . 3
        

     
               |
81 | 79, 80 | eqtri 2109 |
. 2
                      |
82 | 77, 78, 81 | 3eqtr4i 2119 |
1
   
  |