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

Theorem subgrcl 16810
Description: Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
subgrcl  |-  ( S  e.  (SubGrp `  G
)  ->  G  e.  Grp )

Proof of Theorem subgrcl
StepHypRef Expression
1 eqid 2422 . . 3  |-  ( Base `  G )  =  (
Base `  G )
21issubg 16805 . 2  |-  ( S  e.  (SubGrp `  G
)  <->  ( G  e. 
Grp  /\  S  C_  ( Base `  G )  /\  ( Gs  S )  e.  Grp ) )
32simp1bi 1020 1  |-  ( S  e.  (SubGrp `  G
)  ->  G  e.  Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868    C_ wss 3436   ` cfv 5598  (class class class)co 6302   Basecbs 15109   ↾s cress 15110   Grpcgrp 16657  SubGrpcsubg 16799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fv 5606  df-ov 6305  df-subg 16802
This theorem is referenced by:  subg0  16811  subginv  16812  subgmulgcl  16818  subgsubm  16827  subsubg  16828  subgint  16829  isnsg  16834  nsgconj  16838  isnsg3  16839  ssnmz  16847  nmznsg  16849  eqger  16855  eqgid  16857  eqgen  16858  eqgcpbl  16859  qusgrp  16860  quseccl  16861  qusadd  16862  qus0  16863  qusinv  16864  qussub  16865  resghm2  16888  resghm2b  16889  conjsubg  16902  conjsubgen  16903  conjnmz  16904  conjnmzb  16905  qusghm  16907  subgga  16942  gastacos  16952  orbstafun  16953  cntrsubgnsg  16982  oppgsubg  17002  isslw  17248  sylow2blem1  17260  sylow2blem2  17261  sylow2blem3  17262  slwhash  17264  lsmval  17288  lsmelval  17289  lsmelvali  17290  lsmelvalm  17291  lsmsubg  17294  lsmless1  17299  lsmless2  17300  lsmless12  17301  lsmass  17308  lsm01  17309  lsm02  17310  subglsm  17311  lsmmod  17313  lsmcntz  17317  lsmcntzr  17318  lsmdisj2  17320  subgdisj1  17329  pj1f  17335  pj1id  17337  pj1lid  17339  pj1rid  17340  pj1ghm  17341  subgdmdprd  17655  subgdprd  17656  dprdsn  17657  pgpfaclem2  17703  cldsubg  21112
  Copyright terms: Public domain W3C validator