Metamath Proof Explorer


Theorem subgrcl

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

Ref Expression
Assertion subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2 1 issubg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺s 𝑆 ) ∈ Grp ) )
3 2 simp1bi ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )