Metamath Proof Explorer

Theorem submgmacs

Description: Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypothesis submgmacs.b 
|- B = ( Base ` G )
Assertion submgmacs 
|- ( G e. Mgm -> ( SubMgm ` G ) e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 submgmacs.b 
 |-  B = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +g ` G )
3 1 2 issubmgm 
 |-  ( G e. Mgm -> ( s e. ( SubMgm ` G ) <-> ( s C_ B /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) )
4 velpw 
 |-  ( s e. ~P B <-> s C_ B )
5 4 anbi1i 
 |-  ( ( s e. ~P B /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) <-> ( s C_ B /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) )
6 3 5 bitr4di 
 |-  ( G e. Mgm -> ( s e. ( SubMgm ` G ) <-> ( s e. ~P B /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) )
7 6 abbi2dv 
 |-  ( G e. Mgm -> ( SubMgm ` G ) = { s | ( s e. ~P B /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) } )
8 df-rab 
 |-  { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } = { s | ( s e. ~P B /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) }
9 7 8 eqtr4di 
 |-  ( G e. Mgm -> ( SubMgm ` G ) = { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } )
10 1 fvexi 
 |-  B e. _V
11 1 2 mgmcl 
 |-  ( ( G e. Mgm /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
12 11 3expb 
 |-  ( ( G e. Mgm /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B )
13 12 ralrimivva 
 |-  ( G e. Mgm -> A. x e. B A. y e. B ( x ( +g ` G ) y ) e. B )
14 acsfn2 
 |-  ( ( B e. _V /\ A. x e. B A. y e. B ( x ( +g ` G ) y ) e. B ) -> { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } e. ( ACS ` B ) )
15 10 13 14 sylancr 
 |-  ( G e. Mgm -> { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } e. ( ACS ` B ) )
16 9 15 eqeltrd 
 |-  ( G e. Mgm -> ( SubMgm ` G ) e. ( ACS ` B ) )