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 )