1arymaptf

Description: The mapping of unary (endo)functions is a function into 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	1arymaptf	$⊢ X \in V \to H : 1 -aryF X ⟶ X^{X}$

Step	Hyp	Ref	Expression
1		1arymaptfv.h	$⊢ H = (h \in (1 -aryF X) ⟼ (x \in X ⟼ h (\{⟨0, x⟩\})))$
2		fv1arycl	$⊢ (h \in (1 -aryF X) \land x \in X) \to h (\{⟨0, x⟩\}) \in X$
3	2	adantll	$⊢ ((X \in V \land h \in (1 -aryF X)) \land x \in X) \to h (\{⟨0, x⟩\}) \in X$
4	3	fmpttd	$⊢ (X \in V \land h \in (1 -aryF X)) \to (x \in X ⟼ h (\{⟨0, x⟩\})) : X ⟶ X$
5		simpl	$⊢ (X \in V \land h \in (1 -aryF X)) \to X \in V$
6	5 5	elmapd	$⊢ (X \in V \land h \in (1 -aryF X)) \to ((x \in X ⟼ h (\{⟨0, x⟩\})) \in (X^{X}) \leftrightarrow (x \in X ⟼ h (\{⟨0, x⟩\})) : X ⟶ X)$
7	4 6	mpbird	$⊢ (X \in V \land h \in (1 -aryF X)) \to (x \in X ⟼ h (\{⟨0, x⟩\})) \in (X^{X})$
8	7 1	fmptd	$⊢ X \in V \to H : 1 -aryF X ⟶ X^{X}$

Metamath Proof Explorer