Theorem subgrcl 19346

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  ‘cfv 6538  (class class class)co 7420  Basecbs 17392   ↾_s cress 17413  Grpcgrp 19149  SubGrpcsubg 19335

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-subg 19338

This theorem is used by:  subg0  19347  subginv  19348  subgmulgcl  19355  subgsubm  19364  subsubg  19365  subgint  19366  isnsg  19370  nsgconj  19374  isnsg3  19375  ssnmz  19381  nmznsg  19383  eqger  19395  eqgid  19397  eqgen  19398  eqgcpbl  19399  qusgrp  19406  quseccl  19407  qusadd  19408  qus0  19409  qusinv  19410  qussub  19411  ecqusaddcl  19413  resghm2  19452  resghm2b  19453  conjsubg  19469  conjsubgen  19470  conjnmz  19471  conjnmzb  19472  qusghm  19474  ghmqusnsg  19501  ghmquskerlem3  19505  subgga  19519  gastacos  19529  orbstafun  19530  cntrsubgnsg  19562  oppgsubg  19582  isslw  19827  sylow2blem1  19839  sylow2blem2  19840  sylow2blem3  19841  slwhash  19843  lsmval  19867  lsmelval  19868  lsmelvali  19869  lsmelvalm  19870  lsmsubg  19873  lsmless1  19879  lsmless2  19880  lsmless12  19881  lsmass  19888  lsm01  19890  lsm02  19891  subglsm  19892  lsmmod  19894  lsmcntz  19898  lsmcntzr  19899  lsmdisj2  19901  subgdisj1  19910  pj1f  19916  pj1id  19918  pj1lid  19920  pj1rid  19921  pj1ghm  19922  subgdmdprd  20255  subgdprd  20256  dprdsn  20257  pgpfaclem2  20303  cldsubg  24435  gsumsubg  33653  qusker  33956  grplsmid  34001  quslsm  34002  qus0g  34004  qusrn  34006  nsgqus0  34007  nsgmgclem  34008  nsgqusf1olem1  34010  nsgqusf1olem2  34011  nsgqusf1olem3  34012