Metamath Proof Explorer


Theorem efmndbasf

Description: Elements in the monoid of endofunctions on A are functions from A into itself. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndbas.g
|- G = ( EndoFMnd ` A )
efmndbas.b
|- B = ( Base ` G )
Assertion efmndbasf
|- ( F e. B -> F : A --> A )

Proof

Step Hyp Ref Expression
1 efmndbas.g
 |-  G = ( EndoFMnd ` A )
2 efmndbas.b
 |-  B = ( Base ` G )
3 1 2 elefmndbas2
 |-  ( F e. B -> ( F e. B <-> F : A --> A ) )
4 3 ibi
 |-  ( F e. B -> F : A --> A )