Theorem subgrcl 18286

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3938  ‘cfv 6357  (class class class)co 7158  Basecbs 16485   ↾_s cress 16486  Grpcgrp 18105  SubGrpcsubg 18275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fv 6365  df-ov 7161  df-subg 18278

This theorem is referenced by:  subg0  18287  subginv  18288  subgmulgcl  18294  subgsubm  18303  subsubg  18304  subgint  18305  isnsg  18309  nsgconj  18313  isnsg3  18314  ssnmz  18320  nmznsg  18322  eqger  18332  eqgid  18334  eqgen  18335  eqgcpbl  18336  qusgrp  18337  quseccl  18338  qusadd  18339  qus0  18340  qusinv  18341  qussub  18342  resghm2  18377  resghm2b  18378  conjsubg  18392  conjsubgen  18393  conjnmz  18394  conjnmzb  18395  qusghm  18397  subgga  18432  gastacos  18442  orbstafun  18443  cntrsubgnsg  18473  oppgsubg  18493  isslw  18735  sylow2blem1  18747  sylow2blem2  18748  sylow2blem3  18749  slwhash  18751  lsmval  18775  lsmelval  18776  lsmelvali  18777  lsmelvalm  18778  lsmsubg  18781  lsmless1  18787  lsmless2  18788  lsmless12  18789  lsmass  18797  lsm01  18799  lsm02  18800  subglsm  18801  lsmmod  18803  lsmcntz  18807  lsmcntzr  18808  lsmdisj2  18810  subgdisj1  18819  pj1f  18825  pj1id  18827  pj1lid  18829  pj1rid  18830  pj1ghm  18831  subgdmdprd  19158  subgdprd  19159  dprdsn  19160  pgpfaclem2  19206  cldsubg  22721  gsumsubg  30686  qusker  30920