Theorem efmnd1bas

Description: The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024)

	Ref	Expression
Hypotheses	efmnd1bas.1	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmnd1bas.2	$$⊢B={\mathrm{Base}}_G$$
	efmnd1bas.0	$$⊢A=\left\{I\right\}$$
Assertion	efmnd1bas	$$⊢I\in V\to B=\left\{\left\{⟨I,I⟩\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		efmnd1bas.1	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		efmnd1bas.2	$$⊢B={\mathrm{Base}}_G$$
3		efmnd1bas.0	$$⊢A=\left\{I\right\}$$
4	3	fveq2i	Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` { I } ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` { I } ) with typecode |-
5	1 4	eqtri	Could not format G = ( EndoFMnd ` { I } ) : No typesetting found for |- G = ( EndoFMnd ` { I } ) with typecode |-
6	5 2	efmndbas	$$⊢B={\left\{I\right\}}^{\left\{I\right\}}$$
7		fsng	$$⊢\left(I\in V\wedge I\in V\right)\to \left(p:\left\{I\right\}⟶\left\{I\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}\right)$$
8	7	anidms	$$⊢I\in V\to \left(p:\left\{I\right\}⟶\left\{I\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}\right)$$
9		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
10	9 9	elmap	$$⊢p\in \left({\left\{I\right\}}^{\left\{I\right\}}\right)\leftrightarrow p:\left\{I\right\}⟶\left\{I\right\}$$
11		velsn	$$⊢p\in \left\{\left\{⟨I,I⟩\right\}\right\}\leftrightarrow p=\left\{⟨I,I⟩\right\}$$
12	8 10 11	3bitr4g	$$⊢I\in V\to \left(p\in \left({\left\{I\right\}}^{\left\{I\right\}}\right)\leftrightarrow p\in \left\{\left\{⟨I,I⟩\right\}\right\}\right)$$
13	12	eqrdv	$$⊢I\in V\to {\left\{I\right\}}^{\left\{I\right\}}=\left\{\left\{⟨I,I⟩\right\}\right\}$$
14	6 13	syl5eq	$$⊢I\in V\to B=\left\{\left\{⟨I,I⟩\right\}\right\}$$