Description: Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | subgrcl | ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) | |
2 | 1 | issubg | ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) ) |
3 | 2 | simp1bi | ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |