Proof of Theorem curry1
Step | Hyp | Ref
| Expression |
1 | | fnfun 5509 |
. . . . 5
     |
2 | | 2ndconst 6403 |
. . . . . 6
                 |
3 | | dff1o3 5647 |
. . . . . . 7
 
  
                        
 
  
     |
4 | 3 | simprbi 451 |
. . . . . 6
 
  
         
         |
5 | 2, 4 | syl 16 |
. . . . 5
          |
6 | | funco 5458 |
. . . . 5
            
  
     |
7 | 1, 5, 6 | syl2an 464 |
. . . 4
   
            |
8 | | dmco 5345 |
. . . . 5

                     |
9 | | fndm 5511 |
. . . . . . . 8
       |
10 | 9 | adantr 452 |
. . . . . . 7
   
     |
11 | 10 | imaeq2d 5170 |
. . . . . 6
   
    
  
                     |
12 | | imacnvcnv 5301 |
. . . . . . . . 9
                           |
13 | | df-ima 4858 |
. . . . . . . . 9
 
  
        
  
      |
14 | | resres 5126 |
. . . . . . . . . 10
 
  
                |
15 | 14 | rneqi 5063 |
. . . . . . . . 9
 
                   |
16 | 12, 13, 15 | 3eqtri 2436 |
. . . . . . . 8
                         |
17 | | inxp 4974 |
. . . . . . . . . . . . 13
    
            |
18 | | incom 3501 |
. . . . . . . . . . . . . . 15
     |
19 | | inv1 3622 |
. . . . . . . . . . . . . . 15
   |
20 | 18, 19 | eqtri 2432 |
. . . . . . . . . . . . . 14
   |
21 | 20 | xpeq2i 4866 |
. . . . . . . . . . . . 13
               |
22 | 17, 21 | eqtri 2432 |
. . . . . . . . . . . 12
    
          |
23 | | snssi 3910 |
. . . . . . . . . . . . . 14
     |
24 | | df-ss 3302 |
. . . . . . . . . . . . . 14
           |
25 | 23, 24 | sylib 189 |
. . . . . . . . . . . . 13
         |
26 | 25 | xpeq1d 4868 |
. . . . . . . . . . . 12
             |
27 | 22, 26 | syl5eq 2456 |
. . . . . . . . . . 11
               |
28 | 27 | reseq2d 5113 |
. . . . . . . . . 10
                   |
29 | 28 | rneqd 5064 |
. . . . . . . . 9
 
                 |
30 | | 2ndconst 6403 |
. . . . . . . . . 10
                 |
31 | | f1ofo 5648 |
. . . . . . . . . 10
 
  
         
                |
32 | | forn 5623 |
. . . . . . . . . 10
 
  
                  |
33 | 30, 31, 32 | 3syl 19 |
. . . . . . . . 9
 
  
    |
34 | 29, 33 | eqtrd 2444 |
. . . . . . . 8
 
           |
35 | 16, 34 | syl5eq 2456 |
. . . . . . 7
                 |
36 | 35 | adantl 453 |
. . . . . 6
   
    
  
         |
37 | 11, 36 | eqtrd 2444 |
. . . . 5
   
    
  
       |
38 | 8, 37 | syl5eq 2456 |
. . . 4
   
            |
39 | | curry1.1 |
. . . . . 6
  
  
    |
40 | 39 | fneq1i 5506 |
. . . . 5

           |
41 | | df-fn 5424 |
. . . . 5
   
  
               
  
      |
42 | 40, 41 | bitri 241 |
. . . 4

 
 
  
   
 
  
      |
43 | 7, 38, 42 | sylanbrc 646 |
. . 3
   
   |
44 | | dffn5 5739 |
. . 3


       |
45 | 43, 44 | sylib 189 |
. 2
   
         |
46 | 39 | fveq1i 5696 |
. . . . 5
                  |
47 | | dff1o4 5649 |
. . . . . . . . 9
 
  
                               |
48 | 2, 47 | sylib 189 |
. . . . . . . 8
  
                   |
49 | 48 | simprd 450 |
. . . . . . 7
  
  
    |
50 | | vex 2927 |
. . . . . . . 8
 |
51 | | fvco2 5765 |
. . . . . . . 8
                                        |
52 | 50, 51 | mpan2 653 |
. . . . . . 7
                                      |
53 | 49, 52 | syl 16 |
. . . . . 6
    
  
           
  
        |
54 | 53 | ad2antlr 708 |
. . . . 5
    


 
                            |
55 | 46, 54 | syl5eq 2456 |
. . . 4
    


                     |
56 | 2 | adantr 452 |
. . . . . . . . 9
 
                 |
57 | | snidg 3807 |
. . . . . . . . . . . 12
     |
58 | 57, 50 | jctir 525 |
. . . . . . . . . . 11
 
     |
59 | | opelxp 4875 |
. . . . . . . . . . 11
  
    
  
   |
60 | 58, 59 | sylibr 204 |
. . . . . . . . . 10
          |
61 | 60 | adantr 452 |
. . . . . . . . 9
 
          |
62 | 56, 61 | jca 519 |
. . . . . . . 8
 
                          |
63 | | fvres 5712 |
. . . . . . . . . . 11
  
      
                    |
64 | 60, 63 | syl 16 |
. . . . . . . . . 10
  
                    |
65 | | op2ndg 6327 |
. . . . . . . . . . 11
 
          |
66 | 50, 65 | mpan2 653 |
. . . . . . . . . 10
          |
67 | 64, 66 | eqtrd 2444 |
. . . . . . . . 9
  
             |
68 | 67 | adantr 452 |
. . . . . . . 8
 
                |
69 | | f1ocnvfv 5983 |
. . . . . . . 8
                                     
                 |
70 | 62, 68, 69 | sylc 58 |
. . . . . . 7
 
                 |
71 | 70 | fveq2d 5699 |
. . . . . 6
 
                         |
72 | 71 | adantll 695 |
. . . . 5
    


                        |
73 | | df-ov 6051 |
. . . . 5
            |
74 | 72, 73 | syl6eqr 2462 |
. . . 4
    


                     |
75 | 55, 74 | eqtrd 2444 |
. . 3
    


          |
76 | 75 | mpteq2dva 4263 |
. 2
   
               |
77 | 45, 76 | eqtrd 2444 |
1
   
         |