Theorem subgrcl 19107

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  ‘cfv 6498  (class class class)co 7367  Basecbs 17179   ↾_s cress 17200  Grpcgrp 18909  SubGrpcsubg 19096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-subg 19099

This theorem is referenced by:  subg0  19108  subginv  19109  subgmulgcl  19115  subgsubm  19124  subsubg  19125  subgint  19126  isnsg  19130  nsgconj  19134  isnsg3  19135  ssnmz  19141  nmznsg  19143  eqger  19153  eqgid  19155  eqgen  19156  eqgcpbl  19157  qusgrp  19161  quseccl  19162  qusadd  19163  qus0  19164  qusinv  19165  qussub  19166  ecqusaddcl  19168  resghm2  19208  resghm2b  19209  conjsubg  19225  conjsubgen  19226  conjnmz  19227  conjnmzb  19228  qusghm  19230  ghmqusnsg  19257  ghmquskerlem3  19261  subgga  19275  gastacos  19285  orbstafun  19286  cntrsubgnsg  19318  oppgsubg  19338  isslw  19583  sylow2blem1  19595  sylow2blem2  19596  sylow2blem3  19597  slwhash  19599  lsmval  19623  lsmelval  19624  lsmelvali  19625  lsmelvalm  19626  lsmsubg  19629  lsmless1  19635  lsmless2  19636  lsmless12  19637  lsmass  19644  lsm01  19646  lsm02  19647  subglsm  19648  lsmmod  19650  lsmcntz  19654  lsmcntzr  19655  lsmdisj2  19657  subgdisj1  19666  pj1f  19672  pj1id  19674  pj1lid  19676  pj1rid  19677  pj1ghm  19678  subgdmdprd  20011  subgdprd  20012  dprdsn  20013  pgpfaclem2  20059  cldsubg  24076  gsumsubg  33107  qusker  33409  grplsmid  33464  quslsm  33465  qus0g  33467  qusrn  33469  nsgqus0  33470  nsgmgclem  33471  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475