Theorem ielefmnd

Description: The identity function restricted to a set A is an element of the base set of the monoid of endofunctions on A . (Contributed by AV, 27-Jan-2024)

	Ref	Expression
Hypothesis	ielefmnd.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
Assertion	ielefmnd	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		ielefmnd.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2		f1oi	⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴
3		f1of	⊢ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 → ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 )
4	2 3	ax-mp	⊢ ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	1 5	elefmndbas	⊢ ( 𝐴 ∈ 𝑉 → ( ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) ↔ ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 ) )
7	4 6	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )