Metamath Proof Explorer

Theorem mgm2mgm

Description: Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020)

Ref Expression
Assertion mgm2mgm 
|- ( M e. MgmALT <-> M e. Mgm )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` M ) = ( Base ` M )
2 eqid 
 |-  ( +g ` M ) = ( +g ` M )
3 1 2 ismgmALT 
 |-  ( M e. MgmALT -> ( M e. MgmALT <-> ( +g ` M ) clLaw ( Base ` M ) ) )
4 fvex 
 |-  ( +g ` M ) e. _V
5 fvex 
 |-  ( Base ` M ) e. _V
6 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 ) ) )
7 4 5 6 mp2an 
 |-  ( ( +g ` M ) clLaw ( Base ` M ) <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) )
8 1 2 ismgm 
 |-  ( M e. MgmALT -> ( M e. Mgm <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) ) )
9 8 biimprd 
 |-  ( M e. MgmALT -> ( A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) -> M e. Mgm ) )
10 7 9 biimtrid 
 |-  ( M e. MgmALT -> ( ( +g ` M ) clLaw ( Base ` M ) -> M e. Mgm ) )
11 3 10 sylbid 
 |-  ( M e. MgmALT -> ( M e. MgmALT -> M e. Mgm ) )
12 11 pm2.43i 
 |-  ( M e. MgmALT -> M e. Mgm )
13 mgmplusgiopALT 
 |-  ( M e. Mgm -> ( +g ` M ) clLaw ( Base ` M ) )
14 1 2 ismgmALT 
 |-  ( M e. Mgm -> ( M e. MgmALT <-> ( +g ` M ) clLaw ( Base ` M ) ) )
15 13 14 mpbird 
 |-  ( M e. Mgm -> M e. MgmALT )
16 12 15 impbii 
 |-  ( M e. MgmALT <-> M e. Mgm )