Theorem subgrcl 18675

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 2738	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2	1	issubg 18670	. 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp))
3	2	simp1bi 1143	1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  ‘cfv 6418  (class class class)co 7255  Basecbs 16840   ↾_s cress 16867  Grpcgrp 18492  SubGrpcsubg 18664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-subg 18667

This theorem is referenced by:  subg0  18676  subginv  18677  subgmulgcl  18683  subgsubm  18692  subsubg  18693  subgint  18694  isnsg  18698  nsgconj  18702  isnsg3  18703  ssnmz  18709  nmznsg  18711  eqger  18721  eqgid  18723  eqgen  18724  eqgcpbl  18725  qusgrp  18726  quseccl  18727  qusadd  18728  qus0  18729  qusinv  18730  qussub  18731  resghm2  18766  resghm2b  18767  conjsubg  18781  conjsubgen  18782  conjnmz  18783  conjnmzb  18784  qusghm  18786  subgga  18821  gastacos  18831  orbstafun  18832  cntrsubgnsg  18862  oppgsubg  18885  isslw  19128  sylow2blem1  19140  sylow2blem2  19141  sylow2blem3  19142  slwhash  19144  lsmval  19168  lsmelval  19169  lsmelvali  19170  lsmelvalm  19171  lsmsubg  19174  lsmless1  19180  lsmless2  19181  lsmless12  19182  lsmass  19190  lsm01  19192  lsm02  19193  subglsm  19194  lsmmod  19196  lsmcntz  19200  lsmcntzr  19201  lsmdisj2  19203  subgdisj1  19212  pj1f  19218  pj1id  19220  pj1lid  19222  pj1rid  19223  pj1ghm  19224  subgdmdprd  19552  subgdprd  19553  dprdsn  19554  pgpfaclem2  19600  cldsubg  23170  gsumsubg  31208  qusker  31451  grplsmid  31494  quslsm  31495  nsgqus0  31497  nsgmgclem  31498  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502