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

Theorem subgrcl 17422
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 2610 . . 3 (Base‘𝐺) = (Base‘𝐺)
21issubg 17417 . 2 (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺s 𝑆) ∈ Grp))
32simp1bi 1069 1 (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wss 3540  cfv 5804  (class class class)co 6549  Basecbs 15695  s cress 15696  Grpcgrp 17245  SubGrpcsubg 17411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-subg 17414
This theorem is referenced by:  subg0  17423  subginv  17424  subgmulgcl  17430  subgsubm  17439  subsubg  17440  subgint  17441  isnsg  17446  nsgconj  17450  isnsg3  17451  ssnmz  17459  nmznsg  17461  eqger  17467  eqgid  17469  eqgen  17470  eqgcpbl  17471  qusgrp  17472  quseccl  17473  qusadd  17474  qus0  17475  qusinv  17476  qussub  17477  resghm2  17500  resghm2b  17501  conjsubg  17515  conjsubgen  17516  conjnmz  17517  conjnmzb  17518  qusghm  17520  subgga  17556  gastacos  17566  orbstafun  17567  cntrsubgnsg  17596  oppgsubg  17616  isslw  17846  sylow2blem1  17858  sylow2blem2  17859  sylow2blem3  17860  slwhash  17862  lsmval  17886  lsmelval  17887  lsmelvali  17888  lsmelvalm  17889  lsmsubg  17892  lsmless1  17897  lsmless2  17898  lsmless12  17899  lsmass  17906  lsm01  17907  lsm02  17908  subglsm  17909  lsmmod  17911  lsmcntz  17915  lsmcntzr  17916  lsmdisj2  17918  subgdisj1  17927  pj1f  17933  pj1id  17935  pj1lid  17937  pj1rid  17938  pj1ghm  17939  subgdmdprd  18256  subgdprd  18257  dprdsn  18258  pgpfaclem2  18304  cldsubg  21724
  Copyright terms: Public domain W3C validator