Theorem subgrcl 19028

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

Assertion

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

Proof of Theorem subgrcl

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  ‘cfv 6486  (class class class)co 7353  Basecbs 17138   ↾_s cress 17159  Grpcgrp 18830  SubGrpcsubg 19017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-subg 19020

This theorem is referenced by:  subg0  19029  subginv  19030  subgmulgcl  19036  subgsubm  19045  subsubg  19046  subgint  19047  isnsg  19052  nsgconj  19056  isnsg3  19057  ssnmz  19063  nmznsg  19065  eqger  19075  eqgid  19077  eqgen  19078  eqgcpbl  19079  qusgrp  19083  quseccl  19084  qusadd  19085  qus0  19086  qusinv  19087  qussub  19088  ecqusaddcl  19090  resghm2  19130  resghm2b  19131  conjsubg  19147  conjsubgen  19148  conjnmz  19149  conjnmzb  19150  qusghm  19152  ghmqusnsg  19179  ghmquskerlem3  19183  subgga  19197  gastacos  19207  orbstafun  19208  cntrsubgnsg  19240  oppgsubg  19260  isslw  19505  sylow2blem1  19517  sylow2blem2  19518  sylow2blem3  19519  slwhash  19521  lsmval  19545  lsmelval  19546  lsmelvali  19547  lsmelvalm  19548  lsmsubg  19551  lsmless1  19557  lsmless2  19558  lsmless12  19559  lsmass  19566  lsm01  19568  lsm02  19569  subglsm  19570  lsmmod  19572  lsmcntz  19576  lsmcntzr  19577  lsmdisj2  19579  subgdisj1  19588  pj1f  19594  pj1id  19596  pj1lid  19598  pj1rid  19599  pj1ghm  19600  subgdmdprd  19933  subgdprd  19934  dprdsn  19935  pgpfaclem2  19981  cldsubg  24014  gsumsubg  33012  qusker  33296  grplsmid  33351  quslsm  33352  qus0g  33354  qusrn  33356  nsgqus0  33357  nsgmgclem  33358  nsgqusf1olem1  33360  nsgqusf1olem2  33361  nsgqusf1olem3  33362