Theorem subgrcl

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

	Ref	Expression
Assertion	subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2	1	issubg	$$⊢S\in \mathrm{SubGrp}\left(G\right)\leftrightarrow \left(G\in \mathrm{Grp}\wedge S\subseteq {\mathrm{Base}}_G\wedge G{\upharpoonright }_{𝑠}S\in \mathrm{Grp}\right)$$
3	2	simp1bi	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$