MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subgrcl Structured version   Visualization version   GIF version

Theorem subgrcl 18275
Description: Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
subgrcl (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)

Proof of Theorem subgrcl
StepHypRef Expression
1 eqid 2822 . . 3 (Base‘𝐺) = (Base‘𝐺)
21issubg 18270 . 2 (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺s 𝑆) ∈ Grp))
32simp1bi 1142 1 (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  wss 3908  cfv 6334  (class class class)co 7140  Basecbs 16474  s cress 16475  Grpcgrp 18094  SubGrpcsubg 18264
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fv 6342  df-ov 7143  df-subg 18267
This theorem is referenced by:  subg0  18276  subginv  18277  subgmulgcl  18283  subgsubm  18292  subsubg  18293  subgint  18294  isnsg  18298  nsgconj  18302  isnsg3  18303  ssnmz  18309  nmznsg  18311  eqger  18321  eqgid  18323  eqgen  18324  eqgcpbl  18325  qusgrp  18326  quseccl  18327  qusadd  18328  qus0  18329  qusinv  18330  qussub  18331  resghm2  18366  resghm2b  18367  conjsubg  18381  conjsubgen  18382  conjnmz  18383  conjnmzb  18384  qusghm  18386  subgga  18421  gastacos  18431  orbstafun  18432  cntrsubgnsg  18462  oppgsubg  18482  isslw  18724  sylow2blem1  18736  sylow2blem2  18737  sylow2blem3  18738  slwhash  18740  lsmval  18764  lsmelval  18765  lsmelvali  18766  lsmelvalm  18767  lsmsubg  18770  lsmless1  18776  lsmless2  18777  lsmless12  18778  lsmass  18786  lsm01  18788  lsm02  18789  subglsm  18790  lsmmod  18792  lsmcntz  18796  lsmcntzr  18797  lsmdisj2  18799  subgdisj1  18808  pj1f  18814  pj1id  18816  pj1lid  18818  pj1rid  18819  pj1ghm  18820  subgdmdprd  19147  subgdprd  19148  dprdsn  19149  pgpfaclem2  19195  cldsubg  22714  gsumsubg  30715  qusker  30950
  Copyright terms: Public domain W3C validator