This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }