Metamath Proof Explorer

Theorem curry1

Description: Composition with ` ``' ( 2nd |`( { C } X. _V ) ) turns any binary operation F with a constant first operand into a function G of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypothesis curry1.1 ⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
Assertion curry1 ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 curry1.1 ⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
2 fnfun ⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → Fun 𝐹 )
3 2ndconst ⊢ ( 𝐶 ∈ 𝐴 → ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V )
4 dff1o3 ⊢ ( ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V ↔ ( ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –onto→ V ∧ Fun ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) )
5 4 simprbi ⊢ ( ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V → Fun ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
6 3 5 syl ⊢ ( 𝐶 ∈ 𝐴 → Fun ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) )
7 funco ⊢ ( ( Fun 𝐹 ∧ Fun ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) → Fun ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) )
8 2 6 7 syl2an ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → Fun ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) )
9 dmco ⊢ dom ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) = ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ dom 𝐹 )
10 fndm ⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → dom 𝐹 = ( 𝐴 × 𝐵 ) )
11 10 adantr ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → dom 𝐹 = ( 𝐴 × 𝐵 ) )
12 11 imaeq2d ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ dom 𝐹 ) = ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) ) )
13 imacnvcnv ⊢ ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) ) = ( ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) )
14 df-ima ⊢ ( ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) ) = ran ( ( 2nd ↾ ( { 𝐶 } × V ) ) ↾ ( 𝐴 × 𝐵 ) )
15 resres ⊢ ( ( 2nd ↾ ( { 𝐶 } × V ) ) ↾ ( 𝐴 × 𝐵 ) ) = ( 2nd ↾ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) )
16 15 rneqi ⊢ ran ( ( 2nd ↾ ( { 𝐶 } × V ) ) ↾ ( 𝐴 × 𝐵 ) ) = ran ( 2nd ↾ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) )
17 13 14 16 3eqtri ⊢ ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) ) = ran ( 2nd ↾ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) )
18 inxp ⊢ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) = ( ( { 𝐶 } ∩ 𝐴 ) × ( V ∩ 𝐵 ) )
19 incom ⊢ ( V ∩ 𝐵 ) = ( 𝐵 ∩ V )
20 inv1 ⊢ ( 𝐵 ∩ V ) = 𝐵
21 19 20 eqtri ⊢ ( V ∩ 𝐵 ) = 𝐵
22 21 xpeq2i ⊢ ( ( { 𝐶 } ∩ 𝐴 ) × ( V ∩ 𝐵 ) ) = ( ( { 𝐶 } ∩ 𝐴 ) × 𝐵 )
23 18 22 eqtri ⊢ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) = ( ( { 𝐶 } ∩ 𝐴 ) × 𝐵 )
24 snssi ⊢ ( 𝐶 ∈ 𝐴 → { 𝐶 } ⊆ 𝐴 )
25 df-ss ⊢ ( { 𝐶 } ⊆ 𝐴 ↔ ( { 𝐶 } ∩ 𝐴 ) = { 𝐶 } )
26 24 25 sylib ⊢ ( 𝐶 ∈ 𝐴 → ( { 𝐶 } ∩ 𝐴 ) = { 𝐶 } )
27 26 xpeq1d ⊢ ( 𝐶 ∈ 𝐴 → ( ( { 𝐶 } ∩ 𝐴 ) × 𝐵 ) = ( { 𝐶 } × 𝐵 ) )
28 23 27 syl5eq ⊢ ( 𝐶 ∈ 𝐴 → ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) = ( { 𝐶 } × 𝐵 ) )
29 28 reseq2d ⊢ ( 𝐶 ∈ 𝐴 → ( 2nd ↾ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) ) = ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) )
30 29 rneqd ⊢ ( 𝐶 ∈ 𝐴 → ran ( 2nd ↾ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) ) = ran ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) )
31 2ndconst ⊢ ( 𝐶 ∈ 𝐴 → ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) : ( { 𝐶 } × 𝐵 ) –1-1-onto→ 𝐵 )
32 f1ofo ⊢ ( ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) : ( { 𝐶 } × 𝐵 ) –1-1-onto→ 𝐵 → ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) : ( { 𝐶 } × 𝐵 ) –onto→ 𝐵 )
33 forn ⊢ ( ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) : ( { 𝐶 } × 𝐵 ) –onto→ 𝐵 → ran ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) = 𝐵 )
34 31 32 33 3syl ⊢ ( 𝐶 ∈ 𝐴 → ran ( 2nd ↾ ( { 𝐶 } × 𝐵 ) ) = 𝐵 )
35 30 34 eqtrd ⊢ ( 𝐶 ∈ 𝐴 → ran ( 2nd ↾ ( ( { 𝐶 } × V ) ∩ ( 𝐴 × 𝐵 ) ) ) = 𝐵 )
36 17 35 syl5eq ⊢ ( 𝐶 ∈ 𝐴 → ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) ) = 𝐵 )
37 36 adantl ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ ( 𝐴 × 𝐵 ) ) = 𝐵 )
38 12 37 eqtrd ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( ◡ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) “ dom 𝐹 ) = 𝐵 )
39 9 38 syl5eq ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → dom ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) = 𝐵 )
40 1 fneq1i ⊢ ( 𝐺 Fn 𝐵 ↔ ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) Fn 𝐵 )
41 df-fn ⊢ ( ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) Fn 𝐵 ↔ ( Fun ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ∧ dom ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) = 𝐵 ) )
42 40 41 bitri ⊢ ( 𝐺 Fn 𝐵 ↔ ( Fun ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ∧ dom ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) = 𝐵 ) )
43 8 39 42 sylanbrc ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 Fn 𝐵 )
44 dffn5 ⊢ ( 𝐺 Fn 𝐵 ↔ 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑥 ) ) )
45 43 44 sylib ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑥 ) ) )
46 1 fveq1i ⊢ ( 𝐺 ‘ 𝑥 ) = ( ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ‘ 𝑥 )
47 dff1o4 ⊢ ( ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V ↔ ( ( 2nd ↾ ( { 𝐶 } × V ) ) Fn ( { 𝐶 } × V ) ∧ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) Fn V ) )
48 3 47 sylib ⊢ ( 𝐶 ∈ 𝐴 → ( ( 2nd ↾ ( { 𝐶 } × V ) ) Fn ( { 𝐶 } × V ) ∧ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) Fn V ) )
49 fvco2 ⊢ ( ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) Fn V ∧ 𝑥 ∈ V ) → ( ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) )
50 49 elvd ⊢ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) Fn V → ( ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) )
51 48 50 simpl2im ⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) )
52 51 ad2antlr ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ∘ ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) )
53 46 52 syl5eq ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) )
54 3 adantr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V )
55 snidg ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ { 𝐶 } )
56 vex ⊢ 𝑥 ∈ V
57 opelxp ⊢ ( ⟨ 𝐶 , 𝑥 ⟩ ∈ ( { 𝐶 } × V ) ↔ ( 𝐶 ∈ { 𝐶 } ∧ 𝑥 ∈ V ) )
58 55 56 57 sylanblrc ⊢ ( 𝐶 ∈ 𝐴 → ⟨ 𝐶 , 𝑥 ⟩ ∈ ( { 𝐶 } × V ) )
59 58 adantr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ⟨ 𝐶 , 𝑥 ⟩ ∈ ( { 𝐶 } × V ) )
60 54 59 jca ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V ∧ ⟨ 𝐶 , 𝑥 ⟩ ∈ ( { 𝐶 } × V ) ) )
61 58 fvresd ⊢ ( 𝐶 ∈ 𝐴 → ( ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ ⟨ 𝐶 , 𝑥 ⟩ ) = ( 2nd ‘ ⟨ 𝐶 , 𝑥 ⟩ ) )
62 op2ndg ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ V ) → ( 2nd ‘ ⟨ 𝐶 , 𝑥 ⟩ ) = 𝑥 )
63 62 elvd ⊢ ( 𝐶 ∈ 𝐴 → ( 2nd ‘ ⟨ 𝐶 , 𝑥 ⟩ ) = 𝑥 )
64 61 63 eqtrd ⊢ ( 𝐶 ∈ 𝐴 → ( ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ ⟨ 𝐶 , 𝑥 ⟩ ) = 𝑥 )
65 64 adantr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ ⟨ 𝐶 , 𝑥 ⟩ ) = 𝑥 )
66 f1ocnvfv ⊢ ( ( ( 2nd ↾ ( { 𝐶 } × V ) ) : ( { 𝐶 } × V ) –1-1-onto→ V ∧ ⟨ 𝐶 , 𝑥 ⟩ ∈ ( { 𝐶 } × V ) ) → ( ( ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ ⟨ 𝐶 , 𝑥 ⟩ ) = 𝑥 → ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) = ⟨ 𝐶 , 𝑥 ⟩ ) )
67 60 65 66 sylc ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) = ⟨ 𝐶 , 𝑥 ⟩ )
68 67 fveq2d ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝑥 ⟩ ) )
69 68 adantll ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝑥 ⟩ ) )
70 df-ov ⊢ ( 𝐶 𝐹 𝑥 ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝑥 ⟩ )
71 69 70 syl6eqr ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ ( 2nd ↾ ( { 𝐶 } × V ) ) ‘ 𝑥 ) ) = ( 𝐶 𝐹 𝑥 ) )
72 53 71 eqtrd ⊢ ( ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐶 𝐹 𝑥 ) )
73 72 mpteq2dva ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )
74 45 73 eqtrd ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )