Theorem subgrcl 19098

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6492  (class class class)co 7360  Basecbs 17170   ↾_s cress 17191  Grpcgrp 18900  SubGrpcsubg 19087

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 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-subg 19090

This theorem is referenced by:  subg0  19099  subginv  19100  subgmulgcl  19106  subgsubm  19115  subsubg  19116  subgint  19117  isnsg  19121  nsgconj  19125  isnsg3  19126  ssnmz  19132  nmznsg  19134  eqger  19144  eqgid  19146  eqgen  19147  eqgcpbl  19148  qusgrp  19152  quseccl  19153  qusadd  19154  qus0  19155  qusinv  19156  qussub  19157  ecqusaddcl  19159  resghm2  19199  resghm2b  19200  conjsubg  19216  conjsubgen  19217  conjnmz  19218  conjnmzb  19219  qusghm  19221  ghmqusnsg  19248  ghmquskerlem3  19252  subgga  19266  gastacos  19276  orbstafun  19277  cntrsubgnsg  19309  oppgsubg  19329  isslw  19574  sylow2blem1  19586  sylow2blem2  19587  sylow2blem3  19588  slwhash  19590  lsmval  19614  lsmelval  19615  lsmelvali  19616  lsmelvalm  19617  lsmsubg  19620  lsmless1  19626  lsmless2  19627  lsmless12  19628  lsmass  19635  lsm01  19637  lsm02  19638  subglsm  19639  lsmmod  19641  lsmcntz  19645  lsmcntzr  19646  lsmdisj2  19648  subgdisj1  19657  pj1f  19663  pj1id  19665  pj1lid  19667  pj1rid  19668  pj1ghm  19669  subgdmdprd  20002  subgdprd  20003  dprdsn  20004  pgpfaclem2  20050  cldsubg  24086  gsumsubg  33122  qusker  33424  grplsmid  33479  quslsm  33480  qus0g  33482  qusrn  33484  nsgqus0  33485  nsgmgclem  33486  nsgqusf1olem1  33488  nsgqusf1olem2  33489  nsgqusf1olem3  33490