Metamath Proof Explorer


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 }