Theorem subgrcl 19080

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

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3945  ‘cfv 6543  (class class class)co 7415  Basecbs 17174   ↾_s cress 17203  Grpcgrp 18884  SubGrpcsubg 19069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7418  df-subg 19072

This theorem is referenced by:  subg0  19081  subginv  19082  subgmulgcl  19088  subgsubm  19097  subsubg  19098  subgint  19099  isnsg  19104  nsgconj  19108  isnsg3  19109  ssnmz  19115  nmznsg  19117  eqger  19127  eqgid  19129  eqgen  19130  eqgcpbl  19131  qusgrp  19135  quseccl  19136  qusadd  19137  qus0  19138  qusinv  19139  qussub  19140  ecqusaddcl  19142  resghm2  19181  resghm2b  19182  conjsubg  19198  conjsubgen  19199  conjnmz  19200  conjnmzb  19201  qusghm  19203  ghmquskerlem3  19231  subgga  19245  gastacos  19255  orbstafun  19256  cntrsubgnsg  19288  oppgsubg  19311  isslw  19557  sylow2blem1  19569  sylow2blem2  19570  sylow2blem3  19571  slwhash  19573  lsmval  19597  lsmelval  19598  lsmelvali  19599  lsmelvalm  19600  lsmsubg  19603  lsmless1  19609  lsmless2  19610  lsmless12  19611  lsmass  19618  lsm01  19620  lsm02  19621  subglsm  19622  lsmmod  19624  lsmcntz  19628  lsmcntzr  19629  lsmdisj2  19631  subgdisj1  19640  pj1f  19646  pj1id  19648  pj1lid  19650  pj1rid  19651  pj1ghm  19652  subgdmdprd  19985  subgdprd  19986  dprdsn  19987  pgpfaclem2  20033  cldsubg  24009  gsumsubg  32755  qusker  33056  grplsmid  33108  quslsm  33110  qus0g  33112  qusrn  33114  nsgqus0  33115  nsgmgclem  33116  nsgqusf1olem1  33118  nsgqusf1olem2  33119  nsgqusf1olem3  33120  ghmqusnsg  33126