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
|- G = ( EndoFMnd ` A )
efmndbas.b
|- B = ( Base ` G )
Assertion elefmndbas
|- ( A e. V -> ( 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 efmndbas
 |-  B = ( A ^m A )
4 3 eleq2i
 |-  ( F e. B <-> F e. ( A ^m A ) )
5 id
 |-  ( A e. V -> A e. V )
6 5 5 elmapd
 |-  ( A e. V -> ( F e. ( A ^m A ) <-> F : A --> A ) )
7 4 6 syl5bb
 |-  ( A e. V -> ( F e. B <-> F : A --> A ) )