1arymaptfo

Description: The mapping of unary (endo)functions is a function onto the set of endofunctions. (Contributed by AV, 18-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	$⊢ H = (h \in (1 -aryF X) ⟼ (x \in X ⟼ h (\{⟨0, x⟩\})))$
2	1	1arymaptf	$⊢ X \in V \to H : 1 -aryF X ⟶ X^{X}$
3		elmapi	$⊢ f \in (X^{X}) \to f : X ⟶ X$
4		eqid	$⊢ (a \in (X^{\{0\}}) ⟼ f (a (0))) = (a \in (X^{\{0\}}) ⟼ f (a (0)))$
5	4	1arympt1	$⊢ (X \in V \land f : X ⟶ X) \to (a \in (X^{\{0\}}) ⟼ f (a (0))) \in (1 -aryF X)$
6	3 5	sylan2	$⊢ (X \in V \land f \in (X^{X})) \to (a \in (X^{\{0\}}) ⟼ f (a (0))) \in (1 -aryF X)$
7		fveq2	$⊢ g = (a \in (X^{\{0\}}) ⟼ f (a (0))) \to H (g) = H ((a \in (X^{\{0\}}) ⟼ f (a (0))))$
8	7	eqeq2d	$⊢ g = (a \in (X^{\{0\}}) ⟼ f (a (0))) \to (f = H (g) \leftrightarrow f = H ((a \in (X^{\{0\}}) ⟼ f (a (0)))))$
9	8	adantl	$⊢ ((X \in V \land f \in (X^{X})) \land g = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \to (f = H (g) \leftrightarrow f = H ((a \in (X^{\{0\}}) ⟼ f (a (0)))))$
10	3	adantl	$⊢ (X \in V \land f \in (X^{X})) \to f : X ⟶ X$
11	10	feqmptd	$⊢ (X \in V \land f \in (X^{X})) \to f = (x \in X ⟼ f (x))$
12		simplr	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to h = (a \in (X^{\{0\}}) ⟼ f (a (0)))$
13		fveq1	$⊢ a = \{⟨0, x⟩\} \to a (0) = \{⟨0, x⟩\} (0)$
14		c0ex	$⊢ 0 \in V$
15		vex	$⊢ x \in V$
16	14 15	fvsn	$⊢ \{⟨0, x⟩\} (0) = x$
17	13 16	eqtrdi	$⊢ a = \{⟨0, x⟩\} \to a (0) = x$
18	17	fveq2d	$⊢ a = \{⟨0, x⟩\} \to f (a (0)) = f (x)$
19	18	adantl	$⊢ ((((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \land a = \{⟨0, x⟩\}) \to f (a (0)) = f (x)$
20	14	a1i	$⊢ (X \in V \land x \in X) \to 0 \in V$
21		simpr	$⊢ (X \in V \land x \in X) \to x \in X$
22	20 21	fsnd	$⊢ (X \in V \land x \in X) \to \{⟨0, x⟩\} : \{0\} ⟶ X$
23		snex	$⊢ \{0\} \in V$
24	23	a1i	$⊢ x \in X \to \{0\} \in V$
25		elmapg	$⊢ (X \in V \land \{0\} \in V) \to (\{⟨0, x⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, x⟩\} : \{0\} ⟶ X)$
26	24 25	sylan2	$⊢ (X \in V \land x \in X) \to (\{⟨0, x⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, x⟩\} : \{0\} ⟶ X)$
27	22 26	mpbird	$⊢ (X \in V \land x \in X) \to \{⟨0, x⟩\} \in (X^{\{0\}})$
28	27	ad4ant14	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to \{⟨0, x⟩\} \in (X^{\{0\}})$
29		fvexd	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to f (x) \in V$
30		nfv	$⊢ Ⅎ a (X \in V \land f \in (X^{X}))$
31		nfmpt1	$⊢ \underline{Ⅎ} a (a \in (X^{\{0\}}) ⟼ f (a (0)))$
32	31	nfeq2	$⊢ Ⅎ a h = (a \in (X^{\{0\}}) ⟼ f (a (0)))$
33	30 32	nfan	$⊢ Ⅎ a ((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0))))$
34		nfv	$⊢ Ⅎ a x \in X$
35	33 34	nfan	$⊢ Ⅎ a (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X)$
36		nfcv	$⊢ \underline{Ⅎ} a \{⟨0, x⟩\}$
37		nfcv	$⊢ \underline{Ⅎ} a f (x)$
38	12 19 28 29 35 36 37	fvmptdf	$⊢ (((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \land x \in X) \to h (\{⟨0, x⟩\}) = f (x)$
39	38	mpteq2dva	$⊢ ((X \in V \land f \in (X^{X})) \land h = (a \in (X^{\{0\}}) ⟼ f (a (0)))) \to (x \in X ⟼ h (\{⟨0, x⟩\})) = (x \in X ⟼ f (x))$
40		simpl	$⊢ (X \in V \land f \in (X^{X})) \to X \in V$
41	40	mptexd	$⊢ (X \in V \land f \in (X^{X})) \to (x \in X ⟼ f (x)) \in V$
42	1 39 6 41	fvmptd2	$⊢ (X \in V \land f \in (X^{X})) \to H ((a \in (X^{\{0\}}) ⟼ f (a (0)))) = (x \in X ⟼ f (x))$
43	11 42	eqtr4d	$⊢ (X \in V \land f \in (X^{X})) \to f = H ((a \in (X^{\{0\}}) ⟼ f (a (0))))$
44	6 9 43	rspcedvd	$⊢ (X \in V \land f \in (X^{X})) \to \exists g \in (1 -aryF X) f = H (g)$
45	44	ralrimiva	$⊢ X \in V \to \forall f \in (X^{X}) \exists g \in (1 -aryF X) f = H (g)$
46		dffo3	$⊢ H : 1 -aryF X \underset{onto}{⟶} X^{X} \leftrightarrow (H : 1 -aryF X ⟶ X^{X} \land \forall f \in (X^{X}) \exists g \in (1 -aryF X) f = H (g))$
47	2 45 46	sylanbrc	$⊢ X \in V \to H : 1 -aryF X \underset{onto}{⟶} X^{X}$

Metamath Proof Explorer

Theorem 1arymaptfo

Proof