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

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 ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐴 )