Theorem efmndbasabf

Description: The base set of the monoid of endofunctions on class A is the set of functions from A into itself. (Contributed by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	efmndbas.g	|- G = ( EndoFMnd ` A )
	efmndbas.b	|- B = ( Base ` G )
Assertion	efmndbasabf	|- B = { f | f : A --> A }

Proof

Step	Hyp	Ref	Expression
1		efmndbas.g	|- G = ( EndoFMnd ` A )
2		efmndbas.b	|- B = ( Base ` G )
3	1 2	efmndbas	|- B = ( A ^m A )
4		mapvalg	|- ( ( A e. _V /\ A e. _V ) -> ( A ^m A ) = { f | f : A --> A } )
5	4	anidms	|- ( A e. _V -> ( A ^m A ) = { f | f : A --> A } )
6	3 5	eqtrid	|- ( A e. _V -> B = { f | f : A --> A } )
7		base0	|- (/) = ( Base ` (/) )
8	7	eqcomi	|- ( Base ` (/) ) = (/)
9		fvprc	|- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) )
10	1 9	eqtrid	|- ( -. A e. _V -> G = (/) )
11	10	fveq2d	|- ( -. A e. _V -> ( Base ` G ) = ( Base ` (/) ) )
12	2 11	eqtrid	|- ( -. A e. _V -> B = ( Base ` (/) ) )
13		mapprc	|- ( -. A e. _V -> { f | f : A --> A } = (/) )
14	8 12 13	3eqtr4a	|- ( -. A e. _V -> B = { f | f : A --> A } )
15	6 14	pm2.61i	|- B = { f | f : A --> A }