Proof of Theorem curry1
Step | Hyp | Ref
| Expression |
1 | | fnfun 5671 |
. . . . 5
     |
2 | | 2ndconst 6882 |
. . . . . 6
                 |
3 | | dff1o3 5818 |
. . . . . . 7
 
  
                        
 
  
     |
4 | 3 | simprbi 466 |
. . . . . 6
 
  
         
         |
5 | 2, 4 | syl 17 |
. . . . 5
          |
6 | | funco 5619 |
. . . . 5
            
  
     |
7 | 1, 5, 6 | syl2an 480 |
. . . 4
   
            |
8 | | dmco 5342 |
. . . . 5

                     |
9 | | fndm 5673 |
. . . . . . . 8
       |
10 | 9 | adantr 467 |
. . . . . . 7
   
     |
11 | 10 | imaeq2d 5167 |
. . . . . 6
   
    
  
                     |
12 | | imacnvcnv 5299 |
. . . . . . . . 9
                           |
13 | | df-ima 4846 |
. . . . . . . . 9
 
  
        
  
      |
14 | | resres 5116 |
. . . . . . . . . 10
 
  
                |
15 | 14 | rneqi 5060 |
. . . . . . . . 9
 
                   |
16 | 12, 13, 15 | 3eqtri 2476 |
. . . . . . . 8
                         |
17 | | inxp 4966 |
. . . . . . . . . . . . 13
    
            |
18 | | incom 3624 |
. . . . . . . . . . . . . . 15
     |
19 | | inv1 3760 |
. . . . . . . . . . . . . . 15
   |
20 | 18, 19 | eqtri 2472 |
. . . . . . . . . . . . . 14
   |
21 | 20 | xpeq2i 4854 |
. . . . . . . . . . . . 13
               |
22 | 17, 21 | eqtri 2472 |
. . . . . . . . . . . 12
    
          |
23 | | snssi 4115 |
. . . . . . . . . . . . . 14
     |
24 | | df-ss 3417 |
. . . . . . . . . . . . . 14
           |
25 | 23, 24 | sylib 200 |
. . . . . . . . . . . . 13
         |
26 | 25 | xpeq1d 4856 |
. . . . . . . . . . . 12
             |
27 | 22, 26 | syl5eq 2496 |
. . . . . . . . . . 11
               |
28 | 27 | reseq2d 5104 |
. . . . . . . . . 10
                   |
29 | 28 | rneqd 5061 |
. . . . . . . . 9
 
                 |
30 | | 2ndconst 6882 |
. . . . . . . . . 10
                 |
31 | | f1ofo 5819 |
. . . . . . . . . 10
 
  
         
                |
32 | | forn 5794 |
. . . . . . . . . 10
 
  
                  |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . 9
 
  
    |
34 | 29, 33 | eqtrd 2484 |
. . . . . . . 8
 
           |
35 | 16, 34 | syl5eq 2496 |
. . . . . . 7
                 |
36 | 35 | adantl 468 |
. . . . . 6
   
    
  
         |
37 | 11, 36 | eqtrd 2484 |
. . . . 5
   
    
  
       |
38 | 8, 37 | syl5eq 2496 |
. . . 4
   
            |
39 | | curry1.1 |
. . . . . 6
  
  
    |
40 | 39 | fneq1i 5668 |
. . . . 5

           |
41 | | df-fn 5584 |
. . . . 5
   
  
               
  
      |
42 | 40, 41 | bitri 253 |
. . . 4

 
 
  
   
 
  
      |
43 | 7, 38, 42 | sylanbrc 669 |
. . 3
   
   |
44 | | dffn5 5908 |
. . 3


       |
45 | 43, 44 | sylib 200 |
. 2
   
         |
46 | 39 | fveq1i 5864 |
. . . . 5
                  |
47 | | dff1o4 5820 |
. . . . . . . . 9
 
  
                               |
48 | 2, 47 | sylib 200 |
. . . . . . . 8
  
                   |
49 | 48 | simprd 465 |
. . . . . . 7
  
  
    |
50 | | vex 3047 |
. . . . . . . 8
 |
51 | | fvco2 5938 |
. . . . . . . 8
                                        |
52 | 50, 51 | mpan2 676 |
. . . . . . 7
                                      |
53 | 49, 52 | syl 17 |
. . . . . 6
    
  
           
  
        |
54 | 53 | ad2antlr 732 |
. . . . 5
    


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


                     |
56 | 2 | adantr 467 |
. . . . . . . . 9
 
                 |
57 | | snidg 3993 |
. . . . . . . . . . . 12
     |
58 | 57, 50 | jctir 541 |
. . . . . . . . . . 11
 
     |
59 | | opelxp 4863 |
. . . . . . . . . . 11
  
    
  
   |
60 | 58, 59 | sylibr 216 |
. . . . . . . . . 10
          |
61 | 60 | adantr 467 |
. . . . . . . . 9
 
          |
62 | 56, 61 | jca 535 |
. . . . . . . 8
 
                          |
63 | | fvres 5877 |
. . . . . . . . . . 11
  
      
                    |
64 | 60, 63 | syl 17 |
. . . . . . . . . 10
  
                    |
65 | | op2ndg 6803 |
. . . . . . . . . . 11
 
          |
66 | 50, 65 | mpan2 676 |
. . . . . . . . . 10
          |
67 | 64, 66 | eqtrd 2484 |
. . . . . . . . 9
  
             |
68 | 67 | adantr 467 |
. . . . . . . 8
 
                |
69 | | f1ocnvfv 6175 |
. . . . . . . 8
                                     
                 |
70 | 62, 68, 69 | sylc 62 |
. . . . . . 7
 
                 |
71 | 70 | fveq2d 5867 |
. . . . . 6
 
                         |
72 | 71 | adantll 719 |
. . . . 5
    


                        |
73 | | df-ov 6291 |
. . . . 5
            |
74 | 72, 73 | syl6eqr 2502 |
. . . 4
    


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


          |
76 | 75 | mpteq2dva 4488 |
. 2
   
               |
77 | 45, 76 | eqtrd 2484 |
1
   
         |