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	$⊢ G = F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}$
	Assertion	curry1	$⊢ (F Fn (A \times B) \land C \in A) \to G = (x \in B ⟼ C F x)$

Proof

Step	Hyp	Ref	Expression
1		curry1.1	$⊢ G = F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}$
2		fnfun	$⊢ F Fn (A \times B) \to Fun F$
3		2ndconst	$⊢ C \in A \to ({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V$
4		dff1o3	$⊢ ({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V \leftrightarrow (({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{onto}{⟶} V \land Fun {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1})$
5	4	simprbi	$⊢ ({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V \to Fun {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}$
6	3 5	syl	$⊢ C \in A \to Fun {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}$
7		funco	$⊢ (Fun F \land Fun {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) \to Fun (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1})$
8	2 6 7	syl2an	$⊢ (F Fn (A \times B) \land C \in A) \to Fun (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1})$
9		dmco	$⊢ dom (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) = {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [dom F]$
10		fndm	$⊢ F Fn (A \times B) \to dom F = A \times B$
11	10	adantr	$⊢ (F Fn (A \times B) \land C \in A) \to dom F = A \times B$
12	11	imaeq2d	$⊢ (F Fn (A \times B) \land C \in A) \to {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [dom F] = {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [A \times B]$
13		imacnvcnv	$⊢ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [A \times B] = ({2^{nd} ↾}_{(\{C\} \times V)}) [A \times B]$
14		df-ima	$⊢ ({2^{nd} ↾}_{(\{C\} \times V)}) [A \times B] = ran ({({2^{nd} ↾}_{(\{C\} \times V)}) ↾}_{(A \times B)})$
15		resres	$⊢ {({2^{nd} ↾}_{(\{C\} \times V)}) ↾}_{(A \times B)} = {2^{nd} ↾}_{((\{C\} \times V) \cap (A \times B))}$
16	15	rneqi	$⊢ ran ({({2^{nd} ↾}_{(\{C\} \times V)}) ↾}_{(A \times B)}) = ran ({2^{nd} ↾}_{((\{C\} \times V) \cap (A \times B))})$
17	13 14 16	3eqtri	$⊢ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [A \times B] = ran ({2^{nd} ↾}_{((\{C\} \times V) \cap (A \times B))})$
18		inxp	$⊢ (\{C\} \times V) \cap (A \times B) = (\{C\} \cap A) \times (V \cap B)$
19		incom	$⊢ V \cap B = B \cap V$
20		inv1	$⊢ B \cap V = B$
21	19 20	eqtri	$⊢ V \cap B = B$
22	21	xpeq2i	$⊢ (\{C\} \cap A) \times (V \cap B) = (\{C\} \cap A) \times B$
23	18 22	eqtri	$⊢ (\{C\} \times V) \cap (A \times B) = (\{C\} \cap A) \times B$
24		snssi	$⊢ C \in A \to \{C\} \subseteq A$
25		df-ss	$⊢ \{C\} \subseteq A \leftrightarrow \{C\} \cap A = \{C\}$
26	24 25	sylib	$⊢ C \in A \to \{C\} \cap A = \{C\}$
27	26	xpeq1d	$⊢ C \in A \to (\{C\} \cap A) \times B = \{C\} \times B$
28	23 27	syl5eq	$⊢ C \in A \to (\{C\} \times V) \cap (A \times B) = \{C\} \times B$
29	28	reseq2d	$⊢ C \in A \to {2^{nd} ↾}_{((\{C\} \times V) \cap (A \times B))} = {2^{nd} ↾}_{(\{C\} \times B)}$
30	29	rneqd	$⊢ C \in A \to ran ({2^{nd} ↾}_{((\{C\} \times V) \cap (A \times B))}) = ran ({2^{nd} ↾}_{(\{C\} \times B)})$
31		2ndconst	$⊢ C \in A \to ({2^{nd} ↾}_{(\{C\} \times B)}) : \{C\} \times B \underset{1-1 onto}{⟶} B$
32		f1ofo	$⊢ ({2^{nd} ↾}_{(\{C\} \times B)}) : \{C\} \times B \underset{1-1 onto}{⟶} B \to ({2^{nd} ↾}_{(\{C\} \times B)}) : \{C\} \times B \underset{onto}{⟶} B$
33		forn	$⊢ ({2^{nd} ↾}_{(\{C\} \times B)}) : \{C\} \times B \underset{onto}{⟶} B \to ran ({2^{nd} ↾}_{(\{C\} \times B)}) = B$
34	31 32 33	3syl	$⊢ C \in A \to ran ({2^{nd} ↾}_{(\{C\} \times B)}) = B$
35	30 34	eqtrd	$⊢ C \in A \to ran ({2^{nd} ↾}_{((\{C\} \times V) \cap (A \times B))}) = B$
36	17 35	syl5eq	$⊢ C \in A \to {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [A \times B] = B$
37	36	adantl	$⊢ (F Fn (A \times B) \land C \in A) \to {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [A \times B] = B$
38	12 37	eqtrd	$⊢ (F Fn (A \times B) \land C \in A) \to {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}^{-1} [dom F] = B$
39	9 38	syl5eq	$⊢ (F Fn (A \times B) \land C \in A) \to dom (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) = B$
40	1	fneq1i	$⊢ G Fn B \leftrightarrow (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) Fn B$
41		df-fn	$⊢ (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) Fn B \leftrightarrow (Fun (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) \land dom (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) = B)$
42	40 41	bitri	$⊢ G Fn B \leftrightarrow (Fun (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) \land dom (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) = B)$
43	8 39 42	sylanbrc	$⊢ (F Fn (A \times B) \land C \in A) \to G Fn B$
44		dffn5	$⊢ G Fn B \leftrightarrow G = (x \in B ⟼ G (x))$
45	43 44	sylib	$⊢ (F Fn (A \times B) \land C \in A) \to G = (x \in B ⟼ G (x))$
46	1	fveq1i	$⊢ G (x) = (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) (x)$
47		dff1o4	$⊢ ({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V \leftrightarrow (({2^{nd} ↾}_{(\{C\} \times V)}) Fn (\{C\} \times V) \land {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} Fn V)$
48	3 47	sylib	$⊢ C \in A \to (({2^{nd} ↾}_{(\{C\} \times V)}) Fn (\{C\} \times V) \land {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} Fn V)$
49		fvco2	$⊢ ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} Fn V \land x \in V) \to (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) (x) = F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x))$
50	49	elvd	$⊢ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} Fn V \to (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) (x) = F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x))$
51	48 50	simpl2im	$⊢ C \in A \to (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) (x) = F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x))$
52	51	ad2antlr	$⊢ ((F Fn (A \times B) \land C \in A) \land x \in B) \to (F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}) (x) = F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x))$
53	46 52	syl5eq	$⊢ ((F Fn (A \times B) \land C \in A) \land x \in B) \to G (x) = F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x))$
54	3	adantr	$⊢ (C \in A \land x \in B) \to ({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V$
55		snidg	$⊢ C \in A \to C \in \{C\}$
56		vex	$⊢ x \in V$
57		opelxp	$⊢ ⟨C, x⟩ \in (\{C\} \times V) \leftrightarrow (C \in \{C\} \land x \in V)$
58	55 56 57	sylanblrc	$⊢ C \in A \to ⟨C, x⟩ \in (\{C\} \times V)$
59	58	adantr	$⊢ (C \in A \land x \in B) \to ⟨C, x⟩ \in (\{C\} \times V)$
60	54 59	jca	$⊢ (C \in A \land x \in B) \to (({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V \land ⟨C, x⟩ \in (\{C\} \times V))$
61	58	fvresd	$⊢ C \in A \to ({2^{nd} ↾}_{(\{C\} \times V)}) (⟨C, x⟩) = 2^{nd} (⟨C, x⟩)$
62		op2ndg	$⊢ (C \in A \land x \in V) \to 2^{nd} (⟨C, x⟩) = x$
63	62	elvd	$⊢ C \in A \to 2^{nd} (⟨C, x⟩) = x$
64	61 63	eqtrd	$⊢ C \in A \to ({2^{nd} ↾}_{(\{C\} \times V)}) (⟨C, x⟩) = x$
65	64	adantr	$⊢ (C \in A \land x \in B) \to ({2^{nd} ↾}_{(\{C\} \times V)}) (⟨C, x⟩) = x$
66		f1ocnvfv	$⊢ (({2^{nd} ↾}_{(\{C\} \times V)}) : \{C\} \times V \underset{1-1 onto}{⟶} V \land ⟨C, x⟩ \in (\{C\} \times V)) \to (({2^{nd} ↾}_{(\{C\} \times V)}) (⟨C, x⟩) = x \to {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x) = ⟨C, x⟩)$
67	60 65 66	sylc	$⊢ (C \in A \land x \in B) \to {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x) = ⟨C, x⟩$
68	67	fveq2d	$⊢ (C \in A \land x \in B) \to F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x)) = F (⟨C, x⟩)$
69	68	adantll	$⊢ ((F Fn (A \times B) \land C \in A) \land x \in B) \to F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x)) = F (⟨C, x⟩)$
70		df-ov	$⊢ C F x = F (⟨C, x⟩)$
71	69 70	syl6eqr	$⊢ ((F Fn (A \times B) \land C \in A) \land x \in B) \to F ({({2^{nd} ↾}_{(\{C\} \times V)})}^{-1} (x)) = C F x$
72	53 71	eqtrd	$⊢ ((F Fn (A \times B) \land C \in A) \land x \in B) \to G (x) = C F x$
73	72	mpteq2dva	$⊢ (F Fn (A \times B) \land C \in A) \to (x \in B ⟼ G (x)) = (x \in B ⟼ C F x)$
74	45 73	eqtrd	$⊢ (F Fn (A \times B) \land C \in A) \to G = (x \in B ⟼ C F x)$

Metamath Proof Explorer

Theorem curry1

Proof