Theorem ielefmnd

Description: The identity function restricted to a set A is an element of the base set of the monoid of endofunctions on A . (Contributed by AV, 27-Jan-2024)

	Ref	Expression
Hypothesis	ielefmnd.g	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion	ielefmnd	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		ielefmnd.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
3		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\to \left({\mathrm{I}\upharpoonright }_A\right):A⟶A$$
4	2 3	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A⟶A$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	1 5	elefmndbas	$$⊢A\in V\to \left({\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G\leftrightarrow \left({\mathrm{I}\upharpoonright }_A\right):A⟶A\right)$$
7	4 6	mpbiri	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G$$