curry2

Description: Composition with ` ``' ( 1st |`( _V X. { C } ) ) turns any binary operation F with a constant second operand into a function G of the first operand only. This transformation is called "currying". (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008)

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

Proof

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

Metamath Proof Explorer

Theorem curry2

Proof