Step | Hyp | Ref
| Expression |
1 | | relco 5122 |
. 2

  |
2 | | funmpt 5249 |
. . 3
   |
3 | | funrel 5228 |
. . 3
   
   |
4 | 2, 3 | ax-mp 5 |
. 2
   |
5 | | fmptco.1 |
. . . . . . . . . . . . 13
 
   |
6 | | eqid 2177 |
. . . . . . . . . . . . 13
     |
7 | 5, 6 | fmptd 5665 |
. . . . . . . . . . . 12
         |
8 | | fmptco.2 |
. . . . . . . . . . . . 13
     |
9 | 8 | feq1d 5347 |
. . . . . . . . . . . 12
               |
10 | 7, 9 | mpbird 167 |
. . . . . . . . . . 11
       |
11 | | ffun 5363 |
. . . . . . . . . . 11
       |
12 | 10, 11 | syl 14 |
. . . . . . . . . 10
   |
13 | | funbrfv 5549 |
. . . . . . . . . . 11

  
       |
14 | 13 | imp 124 |
. . . . . . . . . 10
           |
15 | 12, 14 | sylan 283 |
. . . . . . . . 9
 
         |
16 | 15 | eqcomd 2183 |
. . . . . . . 8
 
         |
17 | 16 | a1d 22 |
. . . . . . 7
 
     
       |
18 | 17 | expimpd 363 |
. . . . . 6
               |
19 | 18 | pm4.71rd 394 |
. . . . 5
       
               |
20 | 19 | exbidv 1825 |
. . . 4
         
                 |
21 | | exsimpl 1617 |
. . . . . . 7
       
  
           |
22 | | isset 2743 |
. . . . . . 7
    

      |
23 | 21, 22 | sylibr 134 |
. . . . . 6
       
  
          |
24 | 23 | a1i 9 |
. . . . 5
                       |
25 | 12 | adantr 276 |
. . . . . . . 8
 
   |
26 | | fdm 5366 |
. . . . . . . . . . 11
       |
27 | 10, 26 | syl 14 |
. . . . . . . . . 10
   |
28 | 27 | eleq2d 2247 |
. . . . . . . . 9
     |
29 | 28 | biimpar 297 |
. . . . . . . 8
 
   |
30 | | funfvex 5527 |
. . . . . . . 8
         |
31 | 25, 29, 30 | syl2anc 411 |
. . . . . . 7
 
       |
32 | 31 | adantrr 479 |
. . . . . 6
 

  ![]_ ]_](_urbrack.gif)         |
33 | 32 | ex 115 |
. . . . 5
     ![]_ ]_](_urbrack.gif)         |
34 | | breq2 4004 |
. . . . . . . . 9
       
         |
35 | | breq1 4003 |
. . . . . . . . 9
       
         |
36 | 34, 35 | anbi12d 473 |
. . . . . . . 8
                  
          |
37 | 36 | ceqsexgv 2866 |
. . . . . . 7
            
  
                     |
38 | | funfvbrb 5624 |
. . . . . . . . . . 11


         |
39 | 12, 38 | syl 14 |
. . . . . . . . . 10
           |
40 | 39, 28 | bitr3d 190 |
. . . . . . . . 9
           |
41 | 8 | fveq1d 5512 |
. . . . . . . . . 10
             |
42 | | fmptco.3 |
. . . . . . . . . 10
     |
43 | | eqidd 2178 |
. . . . . . . . . 10
   |
44 | 41, 42, 43 | breq123d 4014 |
. . . . . . . . 9
                     |
45 | 40, 44 | anbi12d 473 |
. . . . . . . 8
        
                      |
46 | | nfcv 2319 |
. . . . . . . . . . 11
   |
47 | | nfv 1528 |
. . . . . . . . . . . 12
   |
48 | | nffvmpt1 5521 |
. . . . . . . . . . . . . 14
         |
49 | | nfcv 2319 |
. . . . . . . . . . . . . 14
     |
50 | | nfcv 2319 |
. . . . . . . . . . . . . 14
   |
51 | 48, 49, 50 | nfbr 4046 |
. . . . . . . . . . . . 13
             |
52 | | nfcsb1v 3090 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
53 | 52 | nfeq2 2331 |
. . . . . . . . . . . . 13

  ![]_ ]_](_urbrack.gif)  |
54 | 51, 53 | nfbi 1589 |
. . . . . . . . . . . 12
            
  ![]_ ]_](_urbrack.gif)   |
55 | 47, 54 | nfim 1572 |
. . . . . . . . . . 11
  
             ![]_ ]_](_urbrack.gif)    |
56 | | fveq2 5510 |
. . . . . . . . . . . . . 14
               |
57 | 56 | breq1d 4010 |
. . . . . . . . . . . . 13
                         |
58 | | csbeq1a 3066 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
59 | 58 | eqeq2d 2189 |
. . . . . . . . . . . . 13
 
  ![]_ ]_](_urbrack.gif)    |
60 | 57, 59 | bibi12d 235 |
. . . . . . . . . . . 12
            

             ![]_ ]_](_urbrack.gif)     |
61 | 60 | imbi2d 230 |
. . . . . . . . . . 11
  
                        
  ![]_ ]_](_urbrack.gif)      |
62 | | vex 2740 |
. . . . . . . . . . . . . 14
 |
63 | | simpl 109 |
. . . . . . . . . . . . . . . . 17
 
   |
64 | 63 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
 
     |
65 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
 
   |
66 | | fmptco.4 |
. . . . . . . . . . . . . . . . . 18
   |
67 | 66 | adantr 276 |
. . . . . . . . . . . . . . . . 17
 
   |
68 | 65, 67 | eqeq12d 2192 |
. . . . . . . . . . . . . . . 16
 
     |
69 | 64, 68 | anbi12d 473 |
. . . . . . . . . . . . . . 15
 
   

    |
70 | | df-mpt 4063 |
. . . . . . . . . . . . . . 15
     

   |
71 | 69, 70 | brabga 4260 |
. . . . . . . . . . . . . 14
 
           |
72 | 5, 62, 71 | sylancl 413 |
. . . . . . . . . . . . 13
 
      
    |
73 | | simpr 110 |
. . . . . . . . . . . . . . 15
 
   |
74 | 6 | fvmpt2 5594 |
. . . . . . . . . . . . . . 15
 
         |
75 | 73, 5, 74 | syl2anc 411 |
. . . . . . . . . . . . . 14
 
         |
76 | 75 | breq1d 4010 |
. . . . . . . . . . . . 13
 
                   |
77 | 5 | biantrurd 305 |
. . . . . . . . . . . . 13
 
 

    |
78 | 72, 76, 77 | 3bitr4d 220 |
. . . . . . . . . . . 12
 
           
   |
79 | 78 | expcom 116 |
. . . . . . . . . . 11
            
    |
80 | 46, 55, 61, 79 | vtoclgaf 2802 |
. . . . . . . . . 10
            
  ![]_ ]_](_urbrack.gif)     |
81 | 80 | impcom 125 |
. . . . . . . . 9
 
           
  ![]_ ]_](_urbrack.gif)    |
82 | 81 | pm5.32da 452 |
. . . . . . . 8
              
  ![]_ ]_](_urbrack.gif)     |
83 | 45, 82 | bitrd 188 |
. . . . . . 7
        
          ![]_ ]_](_urbrack.gif)     |
84 | 37, 83 | sylan9bbr 463 |
. . . . . 6
 
                   

  ![]_ ]_](_urbrack.gif)     |
85 | 84 | ex 115 |
. . . . 5
                    

  ![]_ ]_](_urbrack.gif)      |
86 | 24, 33, 85 | pm5.21ndd 705 |
. . . 4
               

  ![]_ ]_](_urbrack.gif)     |
87 | 20, 86 | bitrd 188 |
. . 3
         

  ![]_ ]_](_urbrack.gif)     |
88 | | vex 2740 |
. . . 4
 |
89 | 88, 62 | opelco 4794 |
. . 3
                |
90 | | df-mpt 4063 |
. . . . 5
      
   |
91 | 90 | eleq2i 2244 |
. . . 4
     
  
    
    |
92 | | nfv 1528 |
. . . . . 6

 |
93 | 52 | nfeq2 2331 |
. . . . . 6

  ![]_ ]_](_urbrack.gif)  |
94 | 92, 93 | nfan 1565 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)   |
95 | | nfv 1528 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)   |
96 | | eleq1 2240 |
. . . . . 6
 
   |
97 | 58 | eqeq2d 2189 |
. . . . . 6
 
  ![]_ ]_](_urbrack.gif)    |
98 | 96, 97 | anbi12d 473 |
. . . . 5
  
    ![]_ ]_](_urbrack.gif)     |
99 | | eqeq1 2184 |
. . . . . 6
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
100 | 99 | anbi2d 464 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)     |
101 | 94, 95, 88, 62, 98, 100 | opelopabf 4270 |
. . . 4
       

 

  ![]_ ]_](_urbrack.gif)    |
102 | 91, 101 | bitri 184 |
. . 3
     

  ![]_ ]_](_urbrack.gif)    |
103 | 87, 89, 102 | 3bitr4g 223 |
. 2
      
  
     |
104 | 1, 4, 103 | eqrelrdv 4718 |
1
       |