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 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion efmndbasf ( 𝐹𝐵𝐹 : 𝐴𝐴 )

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 elefmndbas2 ( 𝐹𝐵 → ( 𝐹𝐵𝐹 : 𝐴𝐴 ) )
4 3 ibi ( 𝐹𝐵𝐹 : 𝐴𝐴 )