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	⊢ 𝐺 = ( 𝐹 ∘ ^◡ ( 2^nd ↾ ( { 𝐶 } × V ) ) )
	Assertion	curry1	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 𝐹 𝑥 ) ) )

Proof

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

Metamath Proof Explorer

Theorem curry1

Proof