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	|- G = ( EndoFMnd ` A )
	efmnd1bas.2	|- B = ( Base ` G )
	efmnd1bas.0	|- A = { I }
Assertion	efmnd1bas	|- ( I e. V -> B = { { <. I , I >. } } )

Proof

Step	Hyp	Ref	Expression
1		efmnd1bas.1	|- G = ( EndoFMnd ` A )
2		efmnd1bas.2	|- B = ( Base ` G )
3		efmnd1bas.0	|- A = { I }
4	3	fveq2i	|- ( EndoFMnd ` A ) = ( EndoFMnd ` { I } )
5	1 4	eqtri	|- G = ( EndoFMnd ` { I } )
6	5 2	efmndbas	|- B = ( { I } ^m { I } )
7		fsng	|- ( ( I e. V /\ I e. V ) -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) )
8	7	anidms	|- ( I e. V -> ( p : { I } --> { I } <-> p = { <. I , I >. } ) )
9		snex	|- { I } e. _V
10	9 9	elmap	|- ( p e. ( { I } ^m { I } ) <-> p : { I } --> { I } )
11		velsn	|- ( p e. { { <. I , I >. } } <-> p = { <. I , I >. } )
12	8 10 11	3bitr4g	|- ( I e. V -> ( p e. ( { I } ^m { I } ) <-> p e. { { <. I , I >. } } ) )
13	12	eqrdv	|- ( I e. V -> ( { I } ^m { I } ) = { { <. I , I >. } } )
14	6 13	syl5eq	|- ( I e. V -> B = { { <. I , I >. } } )