Theorem efmndmgm

Description: The monoid of endofunctions on a class A is a magma. (Contributed by AV, 28-Jan-2024)

	Ref	Expression
Hypothesis	efmndmgm.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
Assertion	efmndmgm	⊢ 𝐺 ∈ Mgm

Proof

Step	Hyp	Ref	Expression
1		efmndmgm.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4	1 2 3	efmndcl	⊢ ( ( 𝑓 ∈ ( Base ‘ 𝐺 ) ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ∈ ( Base ‘ 𝐺 ) )
5	4	rgen2	⊢ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ∈ ( Base ‘ 𝐺 )
6	1	fvexi	⊢ 𝐺 ∈ V
7	2 3	ismgm	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ Mgm ↔ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ∈ ( Base ‘ 𝐺 ) ) )
8	6 7	ax-mp	⊢ ( 𝐺 ∈ Mgm ↔ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ∈ ( Base ‘ 𝐺 ) )
9	5 8	mpbir	⊢ 𝐺 ∈ Mgm