Metamath Proof Explorer

Theorem subgacs

Description: Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis subgacs.b 
|- B = ( Base ` G )
Assertion subgacs 
|- ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )

Proof

Step Hyp Ref Expression
1 subgacs.b 
 |-  B = ( Base ` G )
2 eqid 
 |-  ( invg ` G ) = ( invg ` G )
3 2 issubg3 
 |-  ( G e. Grp -> ( s e. ( SubGrp ` G ) <-> ( s e. ( SubMnd ` G ) /\ A. x e. s ( ( invg ` G ) ` x ) e. s ) ) )
4 1 submss 
 |-  ( s e. ( SubMnd ` G ) -> s C_ B )
5 4 adantl 
 |-  ( ( G e. Grp /\ s e. ( SubMnd ` G ) ) -> s C_ B )
6 velpw 
 |-  ( s e. ~P B <-> s C_ B )
7 5 6 sylibr 
 |-  ( ( G e. Grp /\ s e. ( SubMnd ` G ) ) -> s e. ~P B )
8 eleq2w 
 |-  ( y = s -> ( ( ( invg ` G ) ` x ) e. y <-> ( ( invg ` G ) ` x ) e. s ) )
9 8 raleqbi1dv 
 |-  ( y = s -> ( A. x e. y ( ( invg ` G ) ` x ) e. y <-> A. x e. s ( ( invg ` G ) ` x ) e. s ) )
10 9 elrab3 
 |-  ( s e. ~P B -> ( s e. { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } <-> A. x e. s ( ( invg ` G ) ` x ) e. s ) )
11 7 10 syl 
 |-  ( ( G e. Grp /\ s e. ( SubMnd ` G ) ) -> ( s e. { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } <-> A. x e. s ( ( invg ` G ) ` x ) e. s ) )
12 11 pm5.32da 
 |-  ( G e. Grp -> ( ( s e. ( SubMnd ` G ) /\ s e. { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) <-> ( s e. ( SubMnd ` G ) /\ A. x e. s ( ( invg ` G ) ` x ) e. s ) ) )
13 3 12 bitr4d 
 |-  ( G e. Grp -> ( s e. ( SubGrp ` G ) <-> ( s e. ( SubMnd ` G ) /\ s e. { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) ) )
14 elin 
 |-  ( s e. ( ( SubMnd ` G ) i^i { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) <-> ( s e. ( SubMnd ` G ) /\ s e. { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) )
15 13 14 bitr4di 
 |-  ( G e. Grp -> ( s e. ( SubGrp ` G ) <-> s e. ( ( SubMnd ` G ) i^i { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) ) )
16 15 eqrdv 
 |-  ( G e. Grp -> ( SubGrp ` G ) = ( ( SubMnd ` G ) i^i { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) )
17 1 fvexi 
 |-  B e. _V
18 mreacs 
 |-  ( B e. _V -> ( ACS ` B ) e. ( Moore ` ~P B ) )
19 17 18 mp1i 
 |-  ( G e. Grp -> ( ACS ` B ) e. ( Moore ` ~P B ) )
20 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
21 1 submacs 
 |-  ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` B ) )
22 20 21 syl 
 |-  ( G e. Grp -> ( SubMnd ` G ) e. ( ACS ` B ) )
23 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
24 23 ralrimiva 
 |-  ( G e. Grp -> A. x e. B ( ( invg ` G ) ` x ) e. B )
25 acsfn1 
 |-  ( ( B e. _V /\ A. x e. B ( ( invg ` G ) ` x ) e. B ) -> { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } e. ( ACS ` B ) )
26 17 24 25 sylancr 
 |-  ( G e. Grp -> { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } e. ( ACS ` B ) )
27 mreincl 
 |-  ( ( ( ACS ` B ) e. ( Moore ` ~P B ) /\ ( SubMnd ` G ) e. ( ACS ` B ) /\ { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } e. ( ACS ` B ) ) -> ( ( SubMnd ` G ) i^i { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) e. ( ACS ` B ) )
28 19 22 26 27 syl3anc 
 |-  ( G e. Grp -> ( ( SubMnd ` G ) i^i { y e. ~P B | A. x e. y ( ( invg ` G ) ` x ) e. y } ) e. ( ACS ` B ) )
29 16 28 eqeltrd 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )