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

  |
2 | | funmpt 5618 |
. . 3
   |
3 | | funrel 5599 |
. . 3
   
   |
4 | 2, 3 | ax-mp 5 |
. 2
   |
5 | | fmptcof2.3 |
. . . . . . . . . . . . 13
   |
6 | | fmptcof2.1 |
. . . . . . . . . . . . 13
   |
7 | | fmptcof2.2 |
. . . . . . . . . . . . 13
   |
8 | | fmptcof2.4 |
. . . . . . . . . . . . . 14
 
  |
9 | 8 | r19.21bi 2757 |
. . . . . . . . . . . . 13
 
   |
10 | | eqid 2451 |
. . . . . . . . . . . . 13
     |
11 | 5, 6, 7, 9, 10 | fmptdF 28255 |
. . . . . . . . . . . 12
         |
12 | | fmptcof2.5 |
. . . . . . . . . . . . 13
     |
13 | 12 | feq1d 5714 |
. . . . . . . . . . . 12
               |
14 | 11, 13 | mpbird 236 |
. . . . . . . . . . 11
       |
15 | | ffun 5731 |
. . . . . . . . . . 11
       |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
   |
17 | | funbrfv 5903 |
. . . . . . . . . . 11

  
       |
18 | 17 | imp 431 |
. . . . . . . . . 10
           |
19 | 16, 18 | sylan 474 |
. . . . . . . . 9
 
         |
20 | 19 | eqcomd 2457 |
. . . . . . . 8
 
         |
21 | 20 | a1d 26 |
. . . . . . 7
 
     
       |
22 | 21 | expimpd 608 |
. . . . . 6
               |
23 | 22 | pm4.71rd 641 |
. . . . 5
       
               |
24 | 23 | exbidv 1768 |
. . . 4
         
                 |
25 | | fvex 5875 |
. . . . . 6
     |
26 | | breq2 4406 |
. . . . . . 7
       
         |
27 | | breq1 4405 |
. . . . . . 7
       
         |
28 | 26, 27 | anbi12d 717 |
. . . . . 6
                  
          |
29 | 25, 28 | ceqsexv 3084 |
. . . . 5
       
  
                    |
30 | | funfvbrb 5995 |
. . . . . . . . 9


         |
31 | 16, 30 | syl 17 |
. . . . . . . 8
           |
32 | | fdm 5733 |
. . . . . . . . . 10
       |
33 | 14, 32 | syl 17 |
. . . . . . . . 9
   |
34 | 33 | eleq2d 2514 |
. . . . . . . 8
     |
35 | 31, 34 | bitr3d 259 |
. . . . . . 7
           |
36 | 12 | fveq1d 5867 |
. . . . . . . 8
             |
37 | | fmptcof2.6 |
. . . . . . . 8
     |
38 | | eqidd 2452 |
. . . . . . . 8
   |
39 | 36, 37, 38 | breq123d 4416 |
. . . . . . 7
                     |
40 | 35, 39 | anbi12d 717 |
. . . . . 6
        
                      |
41 | 6 | nfcri 2586 |
. . . . . . . . . 10

 |
42 | | nffvmpt1 5873 |
. . . . . . . . . . . . 13
         |
43 | | fmptcof2.x |
. . . . . . . . . . . . . 14
   |
44 | 7, 43 | nfmpt 4491 |
. . . . . . . . . . . . 13
     |
45 | | nfcv 2592 |
. . . . . . . . . . . . 13
   |
46 | 42, 44, 45 | nfbr 4447 |
. . . . . . . . . . . 12
             |
47 | | nfcsb1v 3379 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
48 | 47 | nfeq2 2607 |
. . . . . . . . . . . 12

  ![]_ ]_](_urbrack.gif)  |
49 | 46, 48 | nfbi 2017 |
. . . . . . . . . . 11
            
  ![]_ ]_](_urbrack.gif)   |
50 | 5, 49 | nfim 2003 |
. . . . . . . . . 10
  
             ![]_ ]_](_urbrack.gif)    |
51 | 41, 50 | nfim 2003 |
. . . . . . . . 9
              
  ![]_ ]_](_urbrack.gif)     |
52 | | eleq1 2517 |
. . . . . . . . . 10
 
   |
53 | | fveq2 5865 |
. . . . . . . . . . . . 13
               |
54 | 53 | breq1d 4412 |
. . . . . . . . . . . 12
                         |
55 | | csbeq1a 3372 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
56 | 55 | eqeq2d 2461 |
. . . . . . . . . . . 12
 
  ![]_ ]_](_urbrack.gif)    |
57 | 54, 56 | bibi12d 323 |
. . . . . . . . . . 11
            

             ![]_ ]_](_urbrack.gif)     |
58 | 57 | imbi2d 318 |
. . . . . . . . . 10
  
                        
  ![]_ ]_](_urbrack.gif)      |
59 | 52, 58 | imbi12d 322 |
. . . . . . . . 9
              
  

           
  ![]_ ]_](_urbrack.gif)       |
60 | | vex 3048 |
. . . . . . . . . . . 12
 |
61 | | nfv 1761 |
. . . . . . . . . . . . . 14
  |
62 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
63 | | fmptcof2.y |
. . . . . . . . . . . . . . 15
   |
64 | 62, 63 | nfeq 2603 |
. . . . . . . . . . . . . 14
  |
65 | 61, 64 | nfan 2011 |
. . . . . . . . . . . . 13
  
  |
66 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
   |
67 | 66 | eleq1d 2513 |
. . . . . . . . . . . . . 14
 
     |
68 | | simpr 463 |
. . . . . . . . . . . . . . 15
 
   |
69 | | fmptcof2.7 |
. . . . . . . . . . . . . . . 16
   |
70 | 69 | adantr 467 |
. . . . . . . . . . . . . . 15
 
   |
71 | 68, 70 | eqeq12d 2466 |
. . . . . . . . . . . . . 14
 
     |
72 | 67, 71 | anbi12d 717 |
. . . . . . . . . . . . 13
 
   

    |
73 | | df-mpt 4463 |
. . . . . . . . . . . . 13
     

   |
74 | 65, 72, 73 | brabgaf 28216 |
. . . . . . . . . . . 12
 
           |
75 | 9, 60, 74 | sylancl 668 |
. . . . . . . . . . 11
 
      
    |
76 | | simpr 463 |
. . . . . . . . . . . . 13
 
   |
77 | 6 | fvmpt2f 5949 |
. . . . . . . . . . . . 13
 
         |
78 | 76, 9, 77 | syl2anc 667 |
. . . . . . . . . . . 12
 
         |
79 | 78 | breq1d 4412 |
. . . . . . . . . . 11
 
                   |
80 | 9 | biantrurd 511 |
. . . . . . . . . . 11
 
 

    |
81 | 75, 79, 80 | 3bitr4d 289 |
. . . . . . . . . 10
 
           
   |
82 | 81 | expcom 437 |
. . . . . . . . 9
            
    |
83 | 51, 59, 82 | chvar 2106 |
. . . . . . . 8
            
  ![]_ ]_](_urbrack.gif)     |
84 | 83 | impcom 432 |
. . . . . . 7
 
           
  ![]_ ]_](_urbrack.gif)    |
85 | 84 | pm5.32da 647 |
. . . . . 6
              
  ![]_ ]_](_urbrack.gif)     |
86 | 40, 85 | bitrd 257 |
. . . . 5
        
          ![]_ ]_](_urbrack.gif)     |
87 | 29, 86 | syl5bb 261 |
. . . 4
               

  ![]_ ]_](_urbrack.gif)     |
88 | 24, 87 | bitrd 257 |
. . 3
         

  ![]_ ]_](_urbrack.gif)     |
89 | | vex 3048 |
. . . 4
 |
90 | 89, 60 | opelco 5006 |
. . 3
                |
91 | | df-mpt 4463 |
. . . . 5
      
   |
92 | 91 | eleq2i 2521 |
. . . 4
     
  
    
    |
93 | 47 | nfeq2 2607 |
. . . . . 6

  ![]_ ]_](_urbrack.gif)  |
94 | 41, 93 | nfan 2011 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)   |
95 | | nfv 1761 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)   |
96 | 55 | eqeq2d 2461 |
. . . . . 6
 
  ![]_ ]_](_urbrack.gif)    |
97 | 52, 96 | anbi12d 717 |
. . . . 5
  
    ![]_ ]_](_urbrack.gif)     |
98 | | eqeq1 2455 |
. . . . . 6
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
99 | 98 | anbi2d 710 |
. . . . 5
  
  ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)     |
100 | 94, 95, 89, 60, 97, 99 | opelopabf 4726 |
. . . 4
       

 

  ![]_ ]_](_urbrack.gif)    |
101 | 92, 100 | bitri 253 |
. . 3
     

  ![]_ ]_](_urbrack.gif)    |
102 | 88, 90, 101 | 3bitr4g 292 |
. 2
      
  
     |
103 | 1, 4, 102 | eqrelrdv 4931 |
1
       |