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

Metamath Proof Explorer

Theorem mgmcl

Description: Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010) (Revised by AV, 13-Jan-2020)

Ref Expression
Hypotheses mgmcl.b 
|- B = ( Base ` M )
mgmcl.o 
|- .o. = ( +g ` M )
Assertion mgmcl 
|- ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )

Proof

Step Hyp Ref Expression
1 mgmcl.b 
 |-  B = ( Base ` M )
2 mgmcl.o 
 |-  .o. = ( +g ` M )
3 1 2 ismgm 
 |-  ( M e. Mgm -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
4 3 ibi 
 |-  ( M e. Mgm -> A. x e. B A. y e. B ( x .o. y ) e. B )
5 ovrspc2v 
 |-  ( ( ( X e. B /\ Y e. B ) /\ A. x e. B A. y e. B ( x .o. y ) e. B ) -> ( X .o. Y ) e. B )
6 5 expcom 
 |-  ( A. x e. B A. y e. B ( x .o. y ) e. B -> ( ( X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) )
7 4 6 syl 
 |-  ( M e. Mgm -> ( ( X e. B /\ Y e. B ) -> ( X .o. Y ) e. B ) )
8 7 3impib 
 |-  ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )