2arymaptf1

Description: The mapping of binary (endo)functions is a one-to-one function into the set of binary operations. (Contributed by AV, 22-May-2024)

		Ref	Expression
	Hypothesis	2arymaptf.h	$⊢ H = (h \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})))$
	Assertion	2arymaptf1	$⊢ X \in V \to H : 2 -aryF X \underset{1-1}{⟶} X^{(X \times X)}$

Proof

Step	Hyp	Ref	Expression
1		2arymaptf.h	$⊢ H = (h \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})))$
2	1	2arymaptf	$⊢ X \in V \to H : 2 -aryF X ⟶ X^{(X \times X)}$
3	1	2arymaptfv	$⊢ f \in (2 -aryF X) \to H (f) = (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))$
4	3	ad2antrl	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to H (f) = (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))$
5	1	2arymaptfv	$⊢ g \in (2 -aryF X) \to H (g) = (x \in X, y \in X ⟼ g (\{⟨0, x⟩, ⟨1, y⟩\}))$
6	5	ad2antll	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to H (g) = (x \in X, y \in X ⟼ g (\{⟨0, x⟩, ⟨1, y⟩\}))$
7	4 6	eqeq12d	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to (H (f) = H (g) \leftrightarrow (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\})) = (x \in X, y \in X ⟼ g (\{⟨0, x⟩, ⟨1, y⟩\})))$
8		fvex	$⊢ f (\{⟨0, x⟩, ⟨1, y⟩\}) \in V$
9	8	rgen2w	$⊢ \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) \in V$
10		mpo2eqb	$⊢ \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) \in V \to ((x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\})) = (x \in X, y \in X ⟼ g (\{⟨0, x⟩, ⟨1, y⟩\})) \leftrightarrow \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}))$
11	9 10	mp1i	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to ((x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\})) = (x \in X, y \in X ⟼ g (\{⟨0, x⟩, ⟨1, y⟩\})) \leftrightarrow \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}))$
12		2aryfvalel	$⊢ X \in V \to (f \in (2 -aryF X) \leftrightarrow f : X^{\{0, 1\}} ⟶ X)$
13		2aryfvalel	$⊢ X \in V \to (g \in (2 -aryF X) \leftrightarrow g : X^{\{0, 1\}} ⟶ X)$
14	12 13	anbi12d	$⊢ X \in V \to ((f \in (2 -aryF X) \land g \in (2 -aryF X)) \leftrightarrow (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X))$
15		ffn	$⊢ f : X^{\{0, 1\}} ⟶ X \to f Fn (X^{\{0, 1\}})$
16	15	adantr	$⊢ (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \to f Fn (X^{\{0, 1\}})$
17	16	3ad2ant2	$⊢ (X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f Fn (X^{\{0, 1\}})$
18		ffn	$⊢ g : X^{\{0, 1\}} ⟶ X \to g Fn (X^{\{0, 1\}})$
19	18	adantl	$⊢ (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \to g Fn (X^{\{0, 1\}})$
20	19	3ad2ant2	$⊢ (X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to g Fn (X^{\{0, 1\}})$
21		elmapi	$⊢ z \in (X^{\{0, 1\}}) \to z : \{0, 1\} ⟶ X$
22		0ne1	$⊢ 0 \neq 1$
23		c0ex	$⊢ 0 \in V$
24		1ex	$⊢ 1 \in V$
25	23 24	fprb	$⊢ 0 \neq 1 \to (z : \{0, 1\} ⟶ X \leftrightarrow \exists a \in X \exists b \in X z = \{⟨0, a⟩, ⟨1, b⟩\})$
26	22 25	ax-mp	$⊢ z : \{0, 1\} ⟶ X \leftrightarrow \exists a \in X \exists b \in X z = \{⟨0, a⟩, ⟨1, b⟩\}$
27	21 26	sylib	$⊢ z \in (X^{\{0, 1\}}) \to \exists a \in X \exists b \in X z = \{⟨0, a⟩, ⟨1, b⟩\}$
28		opeq2	$⊢ x = a \to ⟨0, x⟩ = ⟨0, a⟩$
29	28	preq1d	$⊢ x = a \to \{⟨0, x⟩, ⟨1, y⟩\} = \{⟨0, a⟩, ⟨1, y⟩\}$
30	29	fveq2d	$⊢ x = a \to f (\{⟨0, x⟩, ⟨1, y⟩\}) = f (\{⟨0, a⟩, ⟨1, y⟩\})$
31	29	fveq2d	$⊢ x = a \to g (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, a⟩, ⟨1, y⟩\})$
32	30 31	eqeq12d	$⊢ x = a \to (f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}) \leftrightarrow f (\{⟨0, a⟩, ⟨1, y⟩\}) = g (\{⟨0, a⟩, ⟨1, y⟩\}))$
33		opeq2	$⊢ y = b \to ⟨1, y⟩ = ⟨1, b⟩$
34	33	preq2d	$⊢ y = b \to \{⟨0, a⟩, ⟨1, y⟩\} = \{⟨0, a⟩, ⟨1, b⟩\}$
35	34	fveq2d	$⊢ y = b \to f (\{⟨0, a⟩, ⟨1, y⟩\}) = f (\{⟨0, a⟩, ⟨1, b⟩\})$
36	34	fveq2d	$⊢ y = b \to g (\{⟨0, a⟩, ⟨1, y⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\})$
37	35 36	eqeq12d	$⊢ y = b \to (f (\{⟨0, a⟩, ⟨1, y⟩\}) = g (\{⟨0, a⟩, ⟨1, y⟩\}) \leftrightarrow f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
38	32 37	rspc2va	$⊢ ((a \in X \land b \in X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\})$
39	38	expcom	$⊢ \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}) \to ((a \in X \land b \in X) \to f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
40	39	3ad2ant3	$⊢ (X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to ((a \in X \land b \in X) \to f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
41	40	com12	$⊢ (a \in X \land b \in X) \to ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
42	41	adantr	$⊢ ((a \in X \land b \in X) \land z = \{⟨0, a⟩, ⟨1, b⟩\}) \to ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
43		fveq2	$⊢ z = \{⟨0, a⟩, ⟨1, b⟩\} \to f (z) = f (\{⟨0, a⟩, ⟨1, b⟩\})$
44		fveq2	$⊢ z = \{⟨0, a⟩, ⟨1, b⟩\} \to g (z) = g (\{⟨0, a⟩, ⟨1, b⟩\})$
45	43 44	eqeq12d	$⊢ z = \{⟨0, a⟩, ⟨1, b⟩\} \to (f (z) = g (z) \leftrightarrow f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
46	45	adantl	$⊢ ((a \in X \land b \in X) \land z = \{⟨0, a⟩, ⟨1, b⟩\}) \to (f (z) = g (z) \leftrightarrow f (\{⟨0, a⟩, ⟨1, b⟩\}) = g (\{⟨0, a⟩, ⟨1, b⟩\}))$
47	42 46	sylibrd	$⊢ ((a \in X \land b \in X) \land z = \{⟨0, a⟩, ⟨1, b⟩\}) \to ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (z) = g (z))$
48	47	ex	$⊢ (a \in X \land b \in X) \to (z = \{⟨0, a⟩, ⟨1, b⟩\} \to ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (z) = g (z)))$
49	48	rexlimivv	$⊢ \exists a \in X \exists b \in X z = \{⟨0, a⟩, ⟨1, b⟩\} \to ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (z) = g (z))$
50	27 49	syl	$⊢ z \in (X^{\{0, 1\}}) \to ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f (z) = g (z))$
51	50	impcom	$⊢ ((X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \land z \in (X^{\{0, 1\}})) \to f (z) = g (z)$
52	17 20 51	eqfnfvd	$⊢ (X \in V \land (f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \land \forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f = g$
53	52	3exp	$⊢ X \in V \to ((f : X^{\{0, 1\}} ⟶ X \land g : X^{\{0, 1\}} ⟶ X) \to (\forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}) \to f = g))$
54	14 53	sylbid	$⊢ X \in V \to ((f \in (2 -aryF X) \land g \in (2 -aryF X)) \to (\forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}) \to f = g))$
55	54	imp	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to (\forall x \in X \forall y \in X f (\{⟨0, x⟩, ⟨1, y⟩\}) = g (\{⟨0, x⟩, ⟨1, y⟩\}) \to f = g)$
56	11 55	sylbid	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to ((x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\})) = (x \in X, y \in X ⟼ g (\{⟨0, x⟩, ⟨1, y⟩\})) \to f = g)$
57	7 56	sylbid	$⊢ (X \in V \land (f \in (2 -aryF X) \land g \in (2 -aryF X))) \to (H (f) = H (g) \to f = g)$
58	57	ralrimivva	$⊢ X \in V \to \forall f \in (2 -aryF X) \forall g \in (2 -aryF X) (H (f) = H (g) \to f = g)$
59		dff13	$⊢ H : 2 -aryF X \underset{1-1}{⟶} X^{(X \times X)} \leftrightarrow (H : 2 -aryF X ⟶ X^{(X \times X)} \land \forall f \in (2 -aryF X) \forall g \in (2 -aryF X) (H (f) = H (g) \to f = g))$
60	2 58 59	sylanbrc	$⊢ X \in V \to H : 2 -aryF X \underset{1-1}{⟶} X^{(X \times X)}$

Metamath Proof Explorer

Theorem 2arymaptf1

Proof