Metamath Proof Explorer


Theorem elefmndbas2

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

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

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 efmndbasabf 𝐵 = { 𝑓𝑓 : 𝐴𝐴 }
4 3 a1i ( 𝐹𝑉𝐵 = { 𝑓𝑓 : 𝐴𝐴 } )
5 4 eleq2d ( 𝐹𝑉 → ( 𝐹𝐵𝐹 ∈ { 𝑓𝑓 : 𝐴𝐴 } ) )
6 feq1 ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴𝐴𝐹 : 𝐴𝐴 ) )
7 eqid { 𝑓𝑓 : 𝐴𝐴 } = { 𝑓𝑓 : 𝐴𝐴 }
8 6 7 elab2g ( 𝐹𝑉 → ( 𝐹 ∈ { 𝑓𝑓 : 𝐴𝐴 } ↔ 𝐹 : 𝐴𝐴 ) )
9 5 8 bitrd ( 𝐹𝑉 → ( 𝐹𝐵𝐹 : 𝐴𝐴 ) )