Theorem 1arymaptfv

Description: The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024)

	Ref	Expression
Hypothesis	1arymaptfv.h	$$⊢H=\left(h\in \left(1\mathrm{-aryF}X\right)⟼\left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)\right)$$
Assertion	1arymaptfv	$$⊢F\in \left(1\mathrm{-aryF}X\right)\to H\left(F\right)=\left(x\in X⟼F\left(\left\{⟨0,x⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1arymaptfv.h	$$⊢H=\left(h\in \left(1\mathrm{-aryF}X\right)⟼\left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)\right)$$
2		fveq1	$$⊢h=F\to h\left(\left\{⟨0,x⟩\right\}\right)=F\left(\left\{⟨0,x⟩\right\}\right)$$
3	2	mpteq2dv	$$⊢h=F\to \left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)=\left(x\in X⟼F\left(\left\{⟨0,x⟩\right\}\right)\right)$$
4		eqid	$$⊢\left(0..^1\right)=\left(0..^1\right)$$
5	4	naryrcl	$$⊢h\in \left(1\mathrm{-aryF}X\right)\to \left(1\in {\mathbb{N}}_0\wedge X\in \mathrm{V}\right)$$
6	5	simprd	$$⊢h\in \left(1\mathrm{-aryF}X\right)\to X\in \mathrm{V}$$
7	6	mptexd	$$⊢h\in \left(1\mathrm{-aryF}X\right)\to \left(x\in X⟼h\left(\left\{⟨0,x⟩\right\}\right)\right)\in \mathrm{V}$$
8	3 1 7	fvmpt3	$$⊢F\in \left(1\mathrm{-aryF}X\right)\to H\left(F\right)=\left(x\in X⟼F\left(\left\{⟨0,x⟩\right\}\right)\right)$$