Metamath Proof Explorer


Theorem elefmndbas

Description: Two ways of saying a function is a mapping of A to itself. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion elefmndbas ( 𝐴𝑉 → ( 𝐹𝐵𝐹 : 𝐴𝐴 ) )

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 efmndbas 𝐵 = ( 𝐴m 𝐴 )
4 3 eleq2i ( 𝐹𝐵𝐹 ∈ ( 𝐴m 𝐴 ) )
5 id ( 𝐴𝑉𝐴𝑉 )
6 5 5 elmapd ( 𝐴𝑉 → ( 𝐹 ∈ ( 𝐴m 𝐴 ) ↔ 𝐹 : 𝐴𝐴 ) )
7 4 6 syl5bb ( 𝐴𝑉 → ( 𝐹𝐵𝐹 : 𝐴𝐴 ) )