curunc

Description: Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021)

		Ref	Expression
	Assertion	curunc	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to curry uncurry F = F$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to F : A ⟶ C^{B}$
2	1	feqmptd	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to F = (x \in A ⟼ F (x))$
3		uncf	$⊢ F : A ⟶ C^{B} \to uncurry F : A \times B ⟶ C$
4	3	fdmd	$⊢ F : A ⟶ C^{B} \to dom uncurry F = A \times B$
5	4	dmeqd	$⊢ F : A ⟶ C^{B} \to dom dom uncurry F = dom (A \times B)$
6		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
7	5 6	sylan9eq	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to dom dom uncurry F = A$
8	7	eqcomd	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to A = dom dom uncurry F$
9		df-mpt	$⊢ (y \in B ⟼ F (x) (y)) = \{⟨y, z⟩ \| (y \in B \land z = F (x) (y))\}$
10		ffvelrn	$⊢ (F : A ⟶ C^{B} \land x \in A) \to F (x) \in (C^{B})$
11		elmapi	$⊢ F (x) \in (C^{B}) \to F (x) : B ⟶ C$
12	10 11	syl	$⊢ (F : A ⟶ C^{B} \land x \in A) \to F (x) : B ⟶ C$
13	12	feqmptd	$⊢ (F : A ⟶ C^{B} \land x \in A) \to F (x) = (y \in B ⟼ F (x) (y))$
14		ffun	$⊢ uncurry F : A \times B ⟶ C \to Fun uncurry F$
15		funbrfv2b	$⊢ Fun uncurry F \to (⟨x, y⟩ uncurry F z \leftrightarrow (⟨x, y⟩ \in dom uncurry F \land uncurry F (⟨x, y⟩) = z))$
16	3 14 15	3syl	$⊢ F : A ⟶ C^{B} \to (⟨x, y⟩ uncurry F z \leftrightarrow (⟨x, y⟩ \in dom uncurry F \land uncurry F (⟨x, y⟩) = z))$
17	16	adantr	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (⟨x, y⟩ uncurry F z \leftrightarrow (⟨x, y⟩ \in dom uncurry F \land uncurry F (⟨x, y⟩) = z))$
18	4	eleq2d	$⊢ F : A ⟶ C^{B} \to (⟨x, y⟩ \in dom uncurry F \leftrightarrow ⟨x, y⟩ \in (A \times B))$
19		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
20	19	baib	$⊢ x \in A \to (⟨x, y⟩ \in (A \times B) \leftrightarrow y \in B)$
21	18 20	sylan9bb	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (⟨x, y⟩ \in dom uncurry F \leftrightarrow y \in B)$
22		df-ov	$⊢ x uncurry F y = uncurry F (⟨x, y⟩)$
23		uncov	$⊢ (x \in V \land y \in V) \to x uncurry F y = F (x) (y)$
24	23	el2v	$⊢ x uncurry F y = F (x) (y)$
25	22 24	eqtr3i	$⊢ uncurry F (⟨x, y⟩) = F (x) (y)$
26	25	eqeq1i	$⊢ uncurry F (⟨x, y⟩) = z \leftrightarrow F (x) (y) = z$
27		eqcom	$⊢ F (x) (y) = z \leftrightarrow z = F (x) (y)$
28	26 27	bitri	$⊢ uncurry F (⟨x, y⟩) = z \leftrightarrow z = F (x) (y)$
29	28	a1i	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (uncurry F (⟨x, y⟩) = z \leftrightarrow z = F (x) (y))$
30	21 29	anbi12d	$⊢ (F : A ⟶ C^{B} \land x \in A) \to ((⟨x, y⟩ \in dom uncurry F \land uncurry F (⟨x, y⟩) = z) \leftrightarrow (y \in B \land z = F (x) (y)))$
31	17 30	bitrd	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (⟨x, y⟩ uncurry F z \leftrightarrow (y \in B \land z = F (x) (y)))$
32	31	opabbidv	$⊢ (F : A ⟶ C^{B} \land x \in A) \to \{⟨y, z⟩ \| ⟨x, y⟩ uncurry F z\} = \{⟨y, z⟩ \| (y \in B \land z = F (x) (y))\}$
33	9 13 32	3eqtr4a	$⊢ (F : A ⟶ C^{B} \land x \in A) \to F (x) = \{⟨y, z⟩ \| ⟨x, y⟩ uncurry F z\}$
34	33	adantlr	$⊢ ((F : A ⟶ C^{B} \land B \neq \emptyset) \land x \in A) \to F (x) = \{⟨y, z⟩ \| ⟨x, y⟩ uncurry F z\}$
35	8 34	mpteq12dva	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to (x \in A ⟼ F (x)) = (x \in dom dom uncurry F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ uncurry F z\})$
36		df-cur	$⊢ curry uncurry F = (x \in dom dom uncurry F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ uncurry F z\})$
37	35 36	eqtr4di	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to (x \in A ⟼ F (x)) = curry uncurry F$
38	2 37	eqtr2d	$⊢ (F : A ⟶ C^{B} \land B \neq \emptyset) \to curry uncurry F = F$

Metamath Proof Explorer

Theorem curunc

Proof