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

Proof

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

Metamath Proof Explorer

Theorem curry2

Proof