This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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