Theorem efmndbasabf

Description: The base set of the monoid of endofunctions on class A is the set of functions from A into itself. (Contributed by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	efmndbas.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
	efmndbas.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	efmndbasabf	⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		efmndbas.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2		efmndbas.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	1 2	efmndbas	⊢ 𝐵 = ( 𝐴 ↑m 𝐴 )
4		mapvalg	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐴 ↑m 𝐴 ) = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } )
5	4	anidms	⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 𝐴 ) = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } )
6	3 5	syl5eq	⊢ ( 𝐴 ∈ V → 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } )
7		base0	⊢ ∅ = ( Base ‘ ∅ )
8	7	eqcomi	⊢ ( Base ‘ ∅ ) = ∅
9		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ )
10	1 9	syl5eq	⊢ ( ¬ 𝐴 ∈ V → 𝐺 = ∅ )
11	10	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
12	2 11	syl5eq	⊢ ( ¬ 𝐴 ∈ V → 𝐵 = ( Base ‘ ∅ ) )
13		mapprc	⊢ ( ¬ 𝐴 ∈ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } = ∅ )
14	8 12 13	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 } )
15	6 14	pm2.61i	⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 }