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 
|- G = ( EndoFMnd ` A )
Assertion efmndmgm 
|- G e. Mgm

Proof

Step Hyp Ref Expression
1 efmndmgm.g 
 |-  G = ( EndoFMnd ` A )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 1 2 3 efmndcl 
 |-  ( ( f e. ( Base ` G ) /\ g e. ( Base ` G ) ) -> ( f ( +g ` G ) g ) e. ( Base ` G ) )
5 4 rgen2 
 |-  A. f e. ( Base ` G ) A. g e. ( Base ` G ) ( f ( +g ` G ) g ) e. ( Base ` G )
6 1 fvexi 
 |-  G e. _V
7 2 3 ismgm 
 |-  ( G e. _V -> ( G e. Mgm <-> A. f e. ( Base ` G ) A. g e. ( Base ` G ) ( f ( +g ` G ) g ) e. ( Base ` G ) ) )
8 6 7 ax-mp 
 |-  ( G e. Mgm <-> A. f e. ( Base ` G ) A. g e. ( Base ` G ) ( f ( +g ` G ) g ) e. ( Base ` G ) )
9 5 8 mpbir 
 |-  G e. Mgm