Theorem curry1 4082

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."

Hypothesis

Ref	Expression
curry1.1	|- G = (F o. `'(2nd |` ({C} X. V)))

Assertion

Ref	Expression
curry1	|- ((F Fn (A X. B) /\ C e. A) -> G = {<.x, y>. | (x e. B /\ y = (CFx))})

Distinct variable groups:   x,y,A   x,B,y   x,C,y   x,F,y

Proof of Theorem curry1

Step	Hyp	Ref	Expression
1		f1ocnvfv 3865	. . . . . . . . 9 |- (((2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V /\ <.C, z>. e. ({C} X. V)) -> (((2nd |` ({C} X. V))` <.C, z>.) = z -> (`'(2nd |` ({C} X. V))` z) = <.C, z>.))
2		2ndconst 4081	. . . . . . . . . . 11 |- (C e. A -> (2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V)
3	2	adantr 389	. . . . . . . . . 10 |- ((C e. A /\ z e. B) -> (2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V)
4		snidg 2423	. . . . . . . . . . . . 13 |- (C e. A -> C e. {C})
5		visset 1804	. . . . . . . . . . . . 13 |- z e. V
6	4, 5	jctir 293	. . . . . . . . . . . 12 |- (C e. A -> (C e. {C} /\ z e. V))
7	5	opelxp 3204	. . . . . . . . . . . 12 |- (<.C, z>. e. ({C} X. V) <-> (C e. {C} /\ z e. V))
8	6, 7	sylibr 200	. . . . . . . . . . 11 |- (C e. A -> <.C, z>. e. ({C} X. V))
9	8	adantr 389	. . . . . . . . . 10 |- ((C e. A /\ z e. B) -> <.C, z>. e. ({C} X. V))
10	3, 9	jca 288	. . . . . . . . 9 |- ((C e. A /\ z e. B) -> ((2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V /\ <.C, z>. e. ({C} X. V)))
11		fvres 3719	. . . . . . . . . . . 12 |- (<.C, z>. e. ({C} X. V) -> ((2nd |` ({C} X. V))` <.C, z>.) = (2nd` <.C, z>.))
12	8, 11	syl 10	. . . . . . . . . . 11 |- (C e. A -> ((2nd |` ({C} X. V))` <.C, z>.) = (2nd` <.C, z>.))
13		op2ndg 4072	. . . . . . . . . . . 12 |- ((C e. A /\ z e. V) -> (2nd` <.C, z>.) = z)
14	5, 13	mpan2 694	. . . . . . . . . . 11 |- (C e. A -> (2nd` <.C, z>.) = z)
15	12, 14	eqtrd 1499	. . . . . . . . . 10 |- (C e. A -> ((2nd |` ({C} X. V))` <.C, z>.) = z)
16	15	adantr 389	. . . . . . . . 9 |- ((C e. A /\ z e. B) -> ((2nd |` ({C} X. V))` <.C, z>.) = z)
17	1, 10, 16	sylc 68	. . . . . . . 8 |- ((C e. A /\ z e. B) -> (`'(2nd |` ({C} X. V))` z) = <.C, z>.)
18	17	fveq2d 3713	. . . . . . 7 |- ((C e. A /\ z e. B) -> (F` (`'(2nd |` ({C} X. V))` z)) = (F` <.C, z>.))
19	18	adantll 392	. . . . . 6 |- (((F Fn (A X. B) /\ C e. A) /\ z e. B) -> (F` (`'(2nd |` ({C} X. V))` z)) = (F` <.C, z>.))
20		df-opr 3950	. . . . . 6 |- (CFz) = (F` <.C, z>.)
21	19, 20	syl6eqr 1517	. . . . 5 |- (((F Fn (A X. B) /\ C e. A) /\ z e. B) -> (F` (`'(2nd |` ({C} X. V))` z)) = (CFz))
22		fvco2 3760	. . . . . . . . 9 |- ((Fun F /\ `'(2nd |` ({C} X. V)) Fn V /\ z e. V) -> ((F o. `'(2nd |` ({C} X. V)))` z) = (F` (`'(2nd |` ({C} X. V))` z)))
23	5, 22	mp3an3 902	. . . . . . . 8 |- ((Fun F /\ `'(2nd |` ({C} X. V)) Fn V) -> ((F o. `'(2nd |` ({C} X. V)))` z) = (F` (`'(2nd |` ({C} X. V))` z)))
24		fnfun 3571	. . . . . . . 8 |- (F Fn (A X. B) -> Fun F)
25		f1o4 3681	. . . . . . . . . 10 |- ((2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V <-> ((2nd |` ({C} X. V)) Fn ({C} X. V) /\ `'(2nd |` ({C} X. V)) Fn V))
26	2, 25	sylib 198	. . . . . . . . 9 |- (C e. A -> ((2nd |` ({C} X. V)) Fn ({C} X. V) /\ `'(2nd |` ({C} X. V)) Fn V))
27	26	pm3.27d 325	. . . . . . . 8 |- (C e. A -> `'(2nd |` ({C} X. V)) Fn V)
28	23, 24, 27	syl2an 454	. . . . . . 7 |- ((F Fn (A X. B) /\ C e. A) -> ((F o. `'(2nd |` ({C} X. V)))` z) = (F` (`'(2nd |` ({C} X. V))` z)))
29	28	adantr 389	. . . . . 6 |- (((F Fn (A X. B) /\ C e. A) /\ z e. B) -> ((F o. `'(2nd |` ({C} X. V)))` z) = (F` (`'(2nd |` ({C} X. V))` z)))
30		curry1.1	. . . . . . 7 |- G = (F o. `'(2nd |` ({C} X. V)))
31	30	fveq1i 3710	. . . . . 6 |- (G` z) = ((F o. `'(2nd |` ({C} X. V)))` z)
32	29, 31	syl5eq 1511	. . . . 5 |- (((F Fn (A X. B) /\ C e. A) /\ z e. B) -> (G` z) = (F` (`'(2nd |` ({C} X. V))` z)))
33		opreq2 3954	. . . . . . 7 |- (x = z -> (CFx) = (CFz))
34		eqid 1468	. . . . . . 7 |- {<.x, y>. | (x e. B /\ y = (CFx))} = {<.x, y>. | (x e. B /\ y = (CFx))}
35		oprex 3968	. . . . . . 7 |- (CFz) e. V
36	33, 34, 35	fvopab4 3765	. . . . . 6 |- (z e. B -> ({<.x, y>. | (x e. B /\ y = (CFx))}` z) = (CFz))
37	36	adantl 388	. . . . 5 |- (((F Fn (A X. B) /\ C e. A) /\ z e. B) -> ({<.x, y>. | (x e. B /\ y = (CFx))}` z) = (CFz))
38	21, 32, 37	3eqtr4d 1509	. . . 4 |- (((F Fn (A X. B) /\ C e. A) /\ z e. B) -> (G` z) = ({<.x, y>. | (x e. B /\ y = (CFx))}` z))
39	38	r19.21aiva 1706	. . 3 |- ((F Fn (A X. B) /\ C e. A) -> A.z e. B (G` z) = ({<.x, y>. | (x e. B /\ y = (CFx))}` z))
40		eqid 1468	. . 3 |- B = B
41	39, 40	jctil 292	. 2 |- ((F Fn (A X. B) /\ C e. A) -> (B = B /\ A.z e. B (G` z) = ({<.x, y>. | (x e. B /\ y = (CFx))}` z)))
42		funco 3536	. . . . . 6 |- ((Fun F /\ Fun `'(2nd |` ({C} X. V))) -> Fun (F o. `'(2nd |` ({C} X. V))))
43		f1o3 3679	. . . . . . . 8 |- ((2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V <-> ((2nd |` ({C} X. V)):({C} X. V)-onto->V /\ Fun `'(2nd |` ({C} X. V))))
44	43	pm3.27bi 326	. . . . . . 7 |- ((2nd |` ({C} X. V)):({C} X. V)-1-1-onto->V -> Fun `'(2nd |` ({C} X. V)))
45	2, 44	syl 10	. . . . . 6 |- (C e. A -> Fun `'(2nd |` ({C} X. V)))
46	42, 24, 45	syl2an 454	. . . . 5 |- ((F Fn (A X. B) /\ C e. A) -> Fun (F o. `'(2nd |` ({C} X. V))))
47		fndm 3573	. . . . . . . . 9 |- (F Fn (A X. B) -> dom F = (A X. B))
48	47	adantr 389	. . . . . . . 8 |- ((F Fn (A X. B) /\ C e. A) -> dom F = (A X. B))
49	48	imaeq2d 3388	. . . . . . 7 |- ((F Fn (A X. B) /\ C e. A) -> (`'`'(2nd |` ({C} X. V))"dom F) = (`'`'(2nd |` ({C} X. V))"(A X. B)))
50		snssi 2457	. . . . . . . . . . . . . . 15 |- (C e. A -> {C} (_ A)
51		df-ss 2043	. . . . . . . . . . . . . . 15 |- ({C} (_ A <-> ({C} i^i A) = {C})
52	50, 51	sylib 198	. . . . . . . . . . . . . 14 |- (C e. A -> ({C} i^i A) = {C})
53		xpeq1 3190	. . . . . . . . . . . . . 14 |- (({C} i^i A) = {C} -> (({C} i^i A) X. B) = ({C} X. B))
54	52, 53	syl 10	. . . . . . . . . . . . 13 |- (C e. A -> (({C} i^i A) X. B) = ({C} X. B))
55		inxp 3259	. . . . . . . . . . . . . 14 |- (({C} X. V) i^i (A X. B)