unccur

Description: Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021)

		Ref	Expression
	Assertion	unccur	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to uncurry curry F = F$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A \times B ⟶ C \to F Fn (A \times B)$
2	1	anim1i	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\})) \to (F Fn (A \times B) \land B \in (V ∖ \{\emptyset\}))$
3	2	3adant3	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to (F Fn (A \times B) \land B \in (V ∖ \{\emptyset\}))$
4		3anass	$⊢ (F Fn (A \times B) \land x \in A \land y \in B) \leftrightarrow (F Fn (A \times B) \land (x \in A \land y \in B))$
5		curfv	$⊢ ((F Fn (A \times B) \land x \in A \land y \in B) \land B \in (V ∖ \{\emptyset\})) \to curry F (x) (y) = x F y$
6	4 5	sylanbr	$⊢ ((F Fn (A \times B) \land (x \in A \land y \in B)) \land B \in (V ∖ \{\emptyset\})) \to curry F (x) (y) = x F y$
7	6	an32s	$⊢ ((F Fn (A \times B) \land B \in (V ∖ \{\emptyset\})) \land (x \in A \land y \in B)) \to curry F (x) (y) = x F y$
8	7	eqeq1d	$⊢ ((F Fn (A \times B) \land B \in (V ∖ \{\emptyset\})) \land (x \in A \land y \in B)) \to (curry F (x) (y) = z \leftrightarrow x F y = z)$
9		eqcom	$⊢ x F y = z \leftrightarrow z = x F y$
10	8 9	syl6bb	$⊢ ((F Fn (A \times B) \land B \in (V ∖ \{\emptyset\})) \land (x \in A \land y \in B)) \to (curry F (x) (y) = z \leftrightarrow z = x F y)$
11	3 10	sylan	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land (x \in A \land y \in B)) \to (curry F (x) (y) = z \leftrightarrow z = x F y)$
12		curf	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to curry F : A ⟶ C^{B}$
13	12	ffvelrnda	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land x \in A) \to curry F (x) \in (C^{B})$
14		elmapfn	$⊢ curry F (x) \in (C^{B}) \to curry F (x) Fn B$
15	13 14	syl	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land x \in A) \to curry F (x) Fn B$
16		fnbrfvb	$⊢ (curry F (x) Fn B \land y \in B) \to (curry F (x) (y) = z \leftrightarrow y curry F (x) z)$
17	15 16	sylan	$⊢ (((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land x \in A) \land y \in B) \to (curry F (x) (y) = z \leftrightarrow y curry F (x) z)$
18	17	anasss	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land (x \in A \land y \in B)) \to (curry F (x) (y) = z \leftrightarrow y curry F (x) z)$
19		ibar	$⊢ (x \in A \land y \in B) \to (z = x F y \leftrightarrow ((x \in A \land y \in B) \land z = x F y))$
20	19	adantl	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land (x \in A \land y \in B)) \to (z = x F y \leftrightarrow ((x \in A \land y \in B) \land z = x F y))$
21	11 18 20	3bitr3d	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land (x \in A \land y \in B)) \to (y curry F (x) z \leftrightarrow ((x \in A \land y \in B) \land z = x F y))$
22		df-br	$⊢ y curry F (x) z \leftrightarrow ⟨y, z⟩ \in curry F (x)$
23		elfvdm	$⊢ ⟨y, z⟩ \in curry F (x) \to x \in dom curry F$
24	22 23	sylbi	$⊢ y curry F (x) z \to x \in dom curry F$
25		fdm	$⊢ curry F : A ⟶ C^{B} \to dom curry F = A$
26	25	eleq2d	$⊢ curry F : A ⟶ C^{B} \to (x \in dom curry F \leftrightarrow x \in A)$
27	26	biimpa	$⊢ (curry F : A ⟶ C^{B} \land x \in dom curry F) \to x \in A$
28	24 27	sylan2	$⊢ (curry F : A ⟶ C^{B} \land y curry F (x) z) \to x \in A$
29		ffvelrn	$⊢ (curry F : A ⟶ C^{B} \land x \in A) \to curry F (x) \in (C^{B})$
30		elmapi	$⊢ curry F (x) \in (C^{B}) \to curry F (x) : B ⟶ C$
31		fdm	$⊢ curry F (x) : B ⟶ C \to dom curry F (x) = B$
32	29 30 31	3syl	$⊢ (curry F : A ⟶ C^{B} \land x \in A) \to dom curry F (x) = B$
33		vex	$⊢ y \in V$
34		vex	$⊢ z \in V$
35	33 34	breldm	$⊢ y curry F (x) z \to y \in dom curry F (x)$
36		eleq2	$⊢ dom curry F (x) = B \to (y \in dom curry F (x) \leftrightarrow y \in B)$
37	36	biimpa	$⊢ (dom curry F (x) = B \land y \in dom curry F (x)) \to y \in B$
38	32 35 37	syl2an	$⊢ ((curry F : A ⟶ C^{B} \land x \in A) \land y curry F (x) z) \to y \in B$
39	38	an32s	$⊢ ((curry F : A ⟶ C^{B} \land y curry F (x) z) \land x \in A) \to y \in B$
40	28 39	mpdan	$⊢ (curry F : A ⟶ C^{B} \land y curry F (x) z) \to y \in B$
41	28 40	jca	$⊢ (curry F : A ⟶ C^{B} \land y curry F (x) z) \to (x \in A \land y \in B)$
42	12 41	sylan	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land y curry F (x) z) \to (x \in A \land y \in B)$
43	42	stoic1a	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land \neg (x \in A \land y \in B)) \to \neg y curry F (x) z$
44		simpl	$⊢ ((x \in A \land y \in B) \land z = x F y) \to (x \in A \land y \in B)$
45	44	con3i	$⊢ \neg (x \in A \land y \in B) \to \neg ((x \in A \land y \in B) \land z = x F y)$
46	45	adantl	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land \neg (x \in A \land y \in B)) \to \neg ((x \in A \land y \in B) \land z = x F y)$
47	43 46	2falsed	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land \neg (x \in A \land y \in B)) \to (y curry F (x) z \leftrightarrow ((x \in A \land y \in B) \land z = x F y))$
48	21 47	pm2.61dan	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to (y curry F (x) z \leftrightarrow ((x \in A \land y \in B) \land z = x F y))$
49	48	oprabbidv	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to \{⟨⟨x, y⟩, z⟩ \| y curry F (x) z\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = x F y)\}$
50		df-unc	$⊢ uncurry curry F = \{⟨⟨x, y⟩, z⟩ \| y curry F (x) z\}$
51		df-mpo	$⊢ (x \in A, y \in B ⟼ x F y) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = x F y)\}$
52	49 50 51	3eqtr4g	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to uncurry curry F = (x \in A, y \in B ⟼ x F y)$
53		fnov	$⊢ F Fn (A \times B) \leftrightarrow F = (x \in A, y \in B ⟼ x F y)$
54	1 53	sylib	$⊢ F : A \times B ⟶ C \to F = (x \in A, y \in B ⟼ x F y)$
55	54	3ad2ant1	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to F = (x \in A, y \in B ⟼ x F y)$
56	52 55	eqtr4d	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to uncurry curry F = F$

Metamath Proof Explorer

Theorem unccur

Proof