Theorem subgrcl 19198

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906  ‘cfv 6538  (class class class)co 7412  Basecbs 17270   ↾_s cress 17291  Grpcgrp 19001  SubGrpcsubg 19187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-subg 19190

This theorem is referenced by:  subg0  19199  subginv  19200  subgmulgcl  19207  subgsubm  19216  subsubg  19217  subgint  19218  isnsg  19222  nsgconj  19226  isnsg3  19227  ssnmz  19233  nmznsg  19235  eqger  19247  eqgid  19249  eqgen  19250  eqgcpbl  19251  qusgrp  19258  quseccl  19259  qusadd  19260  qus0  19261  qusinv  19262  qussub  19263  ecqusaddcl  19265  resghm2  19304  resghm2b  19305  conjsubg  19321  conjsubgen  19322  conjnmz  19323  conjnmzb  19324  qusghm  19326  ghmqusnsg  19353  ghmquskerlem3  19357  subgga  19371  gastacos  19381  orbstafun  19382  cntrsubgnsg  19414  oppgsubg  19434  isslw  19679  sylow2blem1  19691  sylow2blem2  19692  sylow2blem3  19693  slwhash  19695  lsmval  19719  lsmelval  19720  lsmelvali  19721  lsmelvalm  19722  lsmsubg  19725  lsmless1  19731  lsmless2  19732  lsmless12  19733  lsmass  19740  lsm01  19742  lsm02  19743  subglsm  19744  lsmmod  19746  lsmcntz  19750  lsmcntzr  19751  lsmdisj2  19753  subgdisj1  19762  pj1f  19768  pj1id  19770  pj1lid  19772  pj1rid  19773  pj1ghm  19774  subgdmdprd  20107  subgdprd  20108  dprdsn  20109  pgpfaclem2  20155  cldsubg  24249  gsumsubg  33344  qusker  33647  grplsmid  33691  quslsm  33692  qus0g  33694  qusrn  33696  nsgqus0  33697  nsgmgclem  33698  nsgqusf1olem1  33700  nsgqusf1olem2  33701  nsgqusf1olem3  33702