Step | Hyp | Ref
| Expression |
1 | | df-cur 6899 |
. 2
curry              |
2 | | mpt2curryd.c |
. . . . . . 7
  
  |
3 | | mpt2curryd.f |
. . . . . . . 8
 
  |
4 | 3 | dmmpt2ga 6758 |
. . . . . . 7
 

    |
5 | 2, 4 | syl 16 |
. . . . . 6
     |
6 | 5 | dmeqd 5153 |
. . . . 5

    |
7 | | mpt2curryd.n |
. . . . . 6
   |
8 | | dmxp 5169 |
. . . . . 6

    |
9 | 7, 8 | syl 16 |
. . . . 5
     |
10 | 6, 9 | eqtrd 2495 |
. . . 4

  |
11 | 10 | mpteq1d 4484 |
. . 3
                           |
12 | | df-mpt 4463 |
. . . . 5
      
   |
13 | 3 | mpt2fun 6305 |
. . . . . . . 8
 |
14 | | funbrfv2b 5848 |
. . . . . . . 8

                     |
15 | 13, 14 | mp1i 12 |
. . . . . . 7
 
      
               |
16 | 5 | adantr 465 |
. . . . . . . . . 10
 
     |
17 | 16 | eleq2d 2524 |
. . . . . . . . 9
 
    
  
     |
18 | | opelxp 4980 |
. . . . . . . . 9
          |
19 | 17, 18 | syl6bb 261 |
. . . . . . . 8
 
    

    |
20 | 19 | anbi1d 704 |
. . . . . . 7
 
             
 
            |
21 | | an32 796 |
. . . . . . . . 9
  

      
              |
22 | | ancom 450 |
. . . . . . . . 9
          
  
           |
23 | 21, 22 | bitri 249 |
. . . . . . . 8
  

      
              |
24 | | ibar 504 |
. . . . . . . . . . . . 13
        
       
    |
25 | 24 | bicomd 201 |
. . . . . . . . . . . 12
          
      
   |
26 | 25 | adantl 466 |
. . . . . . . . . . 11
 
          
      
   |
27 | 26 | adantr 465 |
. . . . . . . . . 10
              
      
   |
28 | | df-ov 6206 |
. . . . . . . . . . . . 13
            |
29 | | nfcv 2616 |
. . . . . . . . . . . . . . . . 17
   |
30 | | nfcv 2616 |
. . . . . . . . . . . . . . . . 17
   |
31 | | nfcv 2616 |
. . . . . . . . . . . . . . . . . 18
   |
32 | | nfcsb1v 3414 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)  |
33 | 31, 32 | nfcsb 3416 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
34 | | nfcsb1v 3414 |
. . . . . . . . . . . . . . . . 17
  
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
35 | | csbeq1a 3407 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
36 | | csbeq1a 3407 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
37 | 35, 36 | sylan9eq 2515 |
. . . . . . . . . . . . . . . . 17
 
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
38 | 29, 30, 33, 34, 37 | cbvmpt2 6277 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
39 | 3, 38 | eqtri 2483 |
. . . . . . . . . . . . . . 15
 
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
41 | 35 | eqcomd 2462 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
42 | 41 | equcoms 1735 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
43 | 42 | csbeq2dv 3798 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
44 | | csbeq1a 3407 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
45 | 44 | eqcomd 2462 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   |
46 | 45 | equcoms 1735 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
47 | 43, 46 | sylan9eq 2515 |
. . . . . . . . . . . . . . 15
 
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
48 | 47 | adantl 466 |
. . . . . . . . . . . . . 14
   



    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  |
49 | | simpr 461 |
. . . . . . . . . . . . . . 15
 
   |
50 | 49 | adantr 465 |
. . . . . . . . . . . . . 14
       |
51 | | simpr 461 |
. . . . . . . . . . . . . 14
       |
52 | | rsp2 2896 |
. . . . . . . . . . . . . . . 16
 

 
    |
53 | 2, 52 | syl 16 |
. . . . . . . . . . . . . . 15
       |
54 | 53 | impl 620 |
. . . . . . . . . . . . . 14
       |
55 | 40, 48, 50, 51, 54 | ovmpt2d 6331 |
. . . . . . . . . . . . 13
           |
56 | 28, 55 | syl5eqr 2509 |
. . . . . . . . . . . 12
              |
57 | 56 | eqeq1d 2456 |
. . . . . . . . . . 11
            
   |
58 | | eqcom 2463 |
. . . . . . . . . . 11

  |
59 | 57, 58 | syl6bb 261 |
. . . . . . . . . 10
            
   |
60 | 27, 59 | bitrd 253 |
. . . . . . . . 9
              
   |
61 | 60 | pm5.32da 641 |
. . . . . . . 8
 
             
    |
62 | 23, 61 | syl5bb 257 |
. . . . . . 7
 
                  |
63 | 15, 20, 62 | 3bitrrd 280 |
. . . . . 6
 
  
         |
64 | 63 | opabbidv 4466 |
. . . . 5
 
     
 
            |
65 | 12, 64 | syl5req 2508 |
. . . 4
 
               |
66 | 65 | mpteq2dva 4489 |
. . 3
     
             |
67 | 11, 66 | eqtrd 2495 |
. 2
                   |
68 | 1, 67 | syl5eq 2507 |
1
 curry       |