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

Theorem subgrcl 14642
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 2296 . . 3  |-  ( Base `  G )  =  (
Base `  G )
21issubg 14637 . 2  |-  ( S  e.  (SubGrp `  G
)  <->  ( G  e. 
Grp  /\  S  C_  ( Base `  G )  /\  ( Gs  S )  e.  Grp ) )
32simp1bi 970 1  |-  ( S  e.  (SubGrp `  G
)  ->  G  e.  Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165   ` cfv 5271  (class class class)co 5874   Basecbs 13164   ↾s cress 13165   Grpcgrp 14378  SubGrpcsubg 14631
This theorem is referenced by:  subg0  14643  subginv  14644  subgmulgcl  14650  subgsubm  14655  subsubg  14656  subgint  14657  isnsg  14662  nsgconj  14666  isnsg3  14667  ssnmz  14675  nmznsg  14677  eqger  14683  eqgid  14685  eqgen  14686  eqgcpbl  14687  divsgrp  14688  divseccl  14689  divsadd  14690  divs0  14691  divsinv  14692  divssub  14693  resghm2  14716  resghm2b  14717  conjsubg  14730  conjsubgen  14731  conjnmz  14732  conjnmzb  14733  divsghm  14735  subgga  14770  gastacos  14780  orbstafun  14781  cntrsubgnsg  14832  oppgsubg  14852  isslw  14935  sylow2blem1  14947  sylow2blem2  14948  sylow2blem3  14949  slwhash  14951  lsmval  14975  lsmelval  14976  lsmelvali  14977  lsmelvalm  14978  lsmsubg  14981  lsmless1  14986  lsmless2  14987  lsmless12  14988  lsmass  14995  lsm01  14996  lsm02  14997  subglsm  14998  lsmmod  15000  lsmcntz  15004  lsmcntzr  15005  lsmdisj2  15007  subgdisj1  15016  pj1f  15022  pj1id  15024  pj1lid  15026  pj1rid  15027  pj1ghm  15028  subgdmdprd  15285  subgdprd  15286  dprdsn  15287  pgpfaclem2  15333  cldsubg  17809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fv 5279  df-ov 5877  df-subg 14634
  Copyright terms: Public domain W3C validator