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