Metamath Proof Explorer

Theorem mgmplusgiopALT

Description: Slot 2 (group operation) of a magma as extensible structure is a closed operation on the base set. (Contributed by AV, 13-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion mgmplusgiopALT 
|- ( M e. Mgm -> ( +g ` M ) clLaw ( Base ` M ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` M ) = ( Base ` M )
2 eqid 
 |-  ( +g ` M ) = ( +g ` M )
3 1 2 mgmcl 
 |-  ( ( M e. Mgm /\ x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) e. ( Base ` M ) )
4 3 3expb 
 |-  ( ( M e. Mgm /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( x ( +g ` M ) y ) e. ( Base ` M ) )
5 4 ralrimivva 
 |-  ( M e. Mgm -> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) )
6 fvex 
 |-  ( +g ` M ) e. _V
7 fvex 
 |-  ( Base ` M ) e. _V
8 6 7 pm3.2i 
 |-  ( ( +g ` M ) e. _V /\ ( Base ` M ) e. _V )
9 iscllaw 
 |-  ( ( ( +g ` M ) e. _V /\ ( Base ` M ) e. _V ) -> ( ( +g ` M ) clLaw ( Base ` M ) <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) ) )
10 8 9 mp1i 
 |-  ( M e. Mgm -> ( ( +g ` M ) clLaw ( Base ` M ) <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) ) )
11 5 10 mpbird 
 |-  ( M e. Mgm -> ( +g ` M ) clLaw ( Base ` M ) )