2arymaptfo

Description: The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-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	2arymaptfo	$⊢ X \in V \to H : 2 -aryF X \underset{onto}{⟶} 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		elmapi	$⊢ f \in (X^{(X \times X)}) \to f : X \times X ⟶ X$
4		eqid	$⊢ (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)) = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))$
5	4	2arympt	$⊢ (X \in V \land f : X \times X ⟶ X) \to (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)) \in (2 -aryF X)$
6	3 5	sylan2	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)) \in (2 -aryF X)$
7		fveq2	$⊢ g = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)) \to H (g) = H ((a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)))$
8	7	eqeq2d	$⊢ g = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)) \to (f = H (g) \leftrightarrow f = H ((a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))))$
9	8	adantl	$⊢ ((X \in V \land f \in (X^{(X \times X)})) \land g = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \to (f = H (g) \leftrightarrow f = H ((a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))))$
10		elmapfn	$⊢ f \in (X^{(X \times X)}) \to f Fn (X \times X)$
11	10	adantl	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to f Fn (X \times X)$
12		fnov	$⊢ f Fn (X \times X) \leftrightarrow f = (x \in X, y \in X ⟼ x f y)$
13	11 12	sylib	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to f = (x \in X, y \in X ⟼ x f y)$
14		simp1r	$⊢ (((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \land x \in X \land y \in X) \to h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))$
15		fveq1	$⊢ a = \{⟨0, x⟩, ⟨1, y⟩\} \to a (0) = \{⟨0, x⟩, ⟨1, y⟩\} (0)$
16		0ne1	$⊢ 0 \neq 1$
17		c0ex	$⊢ 0 \in V$
18		vex	$⊢ x \in V$
19	17 18	fvpr1	$⊢ 0 \neq 1 \to \{⟨0, x⟩, ⟨1, y⟩\} (0) = x$
20	16 19	ax-mp	$⊢ \{⟨0, x⟩, ⟨1, y⟩\} (0) = x$
21	15 20	eqtrdi	$⊢ a = \{⟨0, x⟩, ⟨1, y⟩\} \to a (0) = x$
22		fveq1	$⊢ a = \{⟨0, x⟩, ⟨1, y⟩\} \to a (1) = \{⟨0, x⟩, ⟨1, y⟩\} (1)$
23		1ex	$⊢ 1 \in V$
24		vex	$⊢ y \in V$
25	23 24	fvpr2	$⊢ 0 \neq 1 \to \{⟨0, x⟩, ⟨1, y⟩\} (1) = y$
26	16 25	ax-mp	$⊢ \{⟨0, x⟩, ⟨1, y⟩\} (1) = y$
27	22 26	eqtrdi	$⊢ a = \{⟨0, x⟩, ⟨1, y⟩\} \to a (1) = y$
28	21 27	oveq12d	$⊢ a = \{⟨0, x⟩, ⟨1, y⟩\} \to a (0) f a (1) = x f y$
29	28	adantl	$⊢ ((((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \land x \in X \land y \in X) \land a = \{⟨0, x⟩, ⟨1, y⟩\}) \to a (0) f a (1) = x f y$
30	17 23	pm3.2i	$⊢ (0 \in V \land 1 \in V)$
31		fprg	$⊢ ((0 \in V \land 1 \in V) \land (x \in X \land y \in X) \land 0 \neq 1) \to \{⟨0, x⟩, ⟨1, y⟩\} : \{0, 1\} ⟶ \{x, y\}$
32	30 16 31	mp3an13	$⊢ (x \in X \land y \in X) \to \{⟨0, x⟩, ⟨1, y⟩\} : \{0, 1\} ⟶ \{x, y\}$
33	32	3adant1	$⊢ (X \in V \land x \in X \land y \in X) \to \{⟨0, x⟩, ⟨1, y⟩\} : \{0, 1\} ⟶ \{x, y\}$
34		prssi	$⊢ (x \in X \land y \in X) \to \{x, y\} \subseteq X$
35	34	3adant1	$⊢ (X \in V \land x \in X \land y \in X) \to \{x, y\} \subseteq X$
36	33 35	fssd	$⊢ (X \in V \land x \in X \land y \in X) \to \{⟨0, x⟩, ⟨1, y⟩\} : \{0, 1\} ⟶ X$
37		simp1	$⊢ (X \in V \land x \in X \land y \in X) \to X \in V$
38		prex	$⊢ \{0, 1\} \in V$
39	38	a1i	$⊢ (X \in V \land x \in X \land y \in X) \to \{0, 1\} \in V$
40	37 39	elmapd	$⊢ (X \in V \land x \in X \land y \in X) \to (\{⟨0, x⟩, ⟨1, y⟩\} \in (X^{\{0, 1\}}) \leftrightarrow \{⟨0, x⟩, ⟨1, y⟩\} : \{0, 1\} ⟶ X)$
41	36 40	mpbird	$⊢ (X \in V \land x \in X \land y \in X) \to \{⟨0, x⟩, ⟨1, y⟩\} \in (X^{\{0, 1\}})$
42	41	3adant1r	$⊢ ((X \in V \land f \in (X^{(X \times X)})) \land x \in X \land y \in X) \to \{⟨0, x⟩, ⟨1, y⟩\} \in (X^{\{0, 1\}})$
43	42	3adant1r	$⊢ (((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \land x \in X \land y \in X) \to \{⟨0, x⟩, ⟨1, y⟩\} \in (X^{\{0, 1\}})$
44		ovexd	$⊢ (((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \land x \in X \land y \in X) \to x f y \in V$
45		nfv	$⊢ Ⅎ a (X \in V \land f \in (X^{(X \times X)}))$
46		nfmpt1	$⊢ \underline{Ⅎ} a (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))$
47	46	nfeq2	$⊢ Ⅎ a h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))$
48	45 47	nfan	$⊢ Ⅎ a ((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)))$
49		nfv	$⊢ Ⅎ a x \in X$
50		nfv	$⊢ Ⅎ a y \in X$
51	48 49 50	nf3an	$⊢ Ⅎ a (((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \land x \in X \land y \in X)$
52		nfcv	$⊢ \underline{Ⅎ} a \{⟨0, x⟩, ⟨1, y⟩\}$
53		nfcv	$⊢ \underline{Ⅎ} a (x f y)$
54	14 29 43 44 51 52 53	fvmptdf	$⊢ (((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \land x \in X \land y \in X) \to h (\{⟨0, x⟩, ⟨1, y⟩\}) = x f y$
55	54	mpoeq3dva	$⊢ ((X \in V \land f \in (X^{(X \times X)})) \land h = (a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) \to (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) = (x \in X, y \in X ⟼ x f y)$
56		mpoexga	$⊢ (X \in V \land X \in V) \to (x \in X, y \in X ⟼ x f y) \in V$
57	56	anidms	$⊢ X \in V \to (x \in X, y \in X ⟼ x f y) \in V$
58	57	adantr	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to (x \in X, y \in X ⟼ x f y) \in V$
59	1 55 6 58	fvmptd2	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to H ((a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1))) = (x \in X, y \in X ⟼ x f y)$
60	13 59	eqtr4d	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to f = H ((a \in (X^{\{0, 1\}}) ⟼ a (0) f a (1)))$
61	6 9 60	rspcedvd	$⊢ (X \in V \land f \in (X^{(X \times X)})) \to \exists g \in (2 -aryF X) f = H (g)$
62	61	ralrimiva	$⊢ X \in V \to \forall f \in (X^{(X \times X)}) \exists g \in (2 -aryF X) f = H (g)$
63		dffo3	$⊢ H : 2 -aryF X \underset{onto}{⟶} X^{(X \times X)} \leftrightarrow (H : 2 -aryF X ⟶ X^{(X \times X)} \land \forall f \in (X^{(X \times X)}) \exists g \in (2 -aryF X) f = H (g))$
64	2 62 63	sylanbrc	$⊢ X \in V \to H : 2 -aryF X \underset{onto}{⟶} X^{(X \times X)}$

Metamath Proof Explorer

Theorem 2arymaptfo

Proof