Metamath Proof Explorer

Theorem 2aryenef

Description: The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024)

		Ref	Expression
	Assertion	2aryenef	$⊢ (2 -aryF X) \approx (X^{(X \times X)})$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ 2 -aryF X \in V$
2	1	mptex	$⊢ (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))) \in V$
3	2	a1i	$⊢ X \in V \to (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))) \in V$
4		eqid	$⊢ (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))) = (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\})))$
5	4	2arymaptf1o	$⊢ X \in V \to (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))) : 2 -aryF X \underset{1-1 onto}{⟶} X^{(X \times X)}$
6		f1oeq1	$⊢ h = (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))) \to (h : 2 -aryF X \underset{1-1 onto}{⟶} X^{(X \times X)} \leftrightarrow (f \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ f (\{⟨0, x⟩, ⟨1, y⟩\}))) : 2 -aryF X \underset{1-1 onto}{⟶} X^{(X \times X)})$
7	3 5 6	spcedv	$⊢ X \in V \to \exists h h : 2 -aryF X \underset{1-1 onto}{⟶} X^{(X \times X)}$
8		bren	$⊢ (2 -aryF X) \approx (X^{(X \times X)}) \leftrightarrow \exists h h : 2 -aryF X \underset{1-1 onto}{⟶} X^{(X \times X)}$
9	7 8	sylibr	$⊢ X \in V \to (2 -aryF X) \approx (X^{(X \times X)})$
10		0ex	$⊢ \emptyset \in V$
11	10	enref	$⊢ \emptyset \approx \emptyset$
12	11	a1i	$⊢ \neg X \in V \to \emptyset \approx \emptyset$
13		df-naryf	$⊢ -aryF = (n \in ℕ_{0}, x \in V ⟼ x^{(x^{(0 ..^n)})})$
14	13	reldmmpo	$⊢ Rel dom -aryF$
15	14	ovprc2	$⊢ \neg X \in V \to 2 -aryF X = \emptyset$
16		reldmmap	$⊢ Rel dom ↑_{𝑚}$
17	16	ovprc1	$⊢ \neg X \in V \to X^{(X \times X)} = \emptyset$
18	12 15 17	3brtr4d	$⊢ \neg X \in V \to (2 -aryF X) \approx (X^{(X \times X)})$
19	9 18	pm2.61i	$⊢ (2 -aryF X) \approx (X^{(X \times X)})$