Metamath Proof Explorer

Theorem subgrcl

Description: Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion subgrcl 
|- ( S e. ( SubGrp ` G ) -> G e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 1 issubg 
 |-  ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ ( Base ` G ) /\ ( G |`s S ) e. Grp ) )
3 2 simp1bi 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )