Theorem subgrcl 19119

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3931  ‘cfv 6541  (class class class)co 7413  Basecbs 17230   ↾_s cress 17253  Grpcgrp 18921  SubGrpcsubg 19108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fv 6549  df-ov 7416  df-subg 19111

This theorem is referenced by:  subg0  19120  subginv  19121  subgmulgcl  19127  subgsubm  19136  subsubg  19137  subgint  19138  isnsg  19143  nsgconj  19147  isnsg3  19148  ssnmz  19154  nmznsg  19156  eqger  19166  eqgid  19168  eqgen  19169  eqgcpbl  19170  qusgrp  19174  quseccl  19175  qusadd  19176  qus0  19177  qusinv  19178  qussub  19179  ecqusaddcl  19181  resghm2  19221  resghm2b  19222  conjsubg  19238  conjsubgen  19239  conjnmz  19240  conjnmzb  19241  qusghm  19243  ghmqusnsg  19270  ghmquskerlem3  19274  subgga  19288  gastacos  19298  orbstafun  19299  cntrsubgnsg  19331  oppgsubg  19351  isslw  19595  sylow2blem1  19607  sylow2blem2  19608  sylow2blem3  19609  slwhash  19611  lsmval  19635  lsmelval  19636  lsmelvali  19637  lsmelvalm  19638  lsmsubg  19641  lsmless1  19647  lsmless2  19648  lsmless12  19649  lsmass  19656  lsm01  19658  lsm02  19659  subglsm  19660  lsmmod  19662  lsmcntz  19666  lsmcntzr  19667  lsmdisj2  19669  subgdisj1  19678  pj1f  19684  pj1id  19686  pj1lid  19688  pj1rid  19689  pj1ghm  19690  subgdmdprd  20023  subgdprd  20024  dprdsn  20025  pgpfaclem2  20071  cldsubg  24066  gsumsubg  32993  qusker  33317  grplsmid  33372  quslsm  33373  qus0g  33375  qusrn  33377  nsgqus0  33378  nsgmgclem  33379  nsgqusf1olem1  33381  nsgqusf1olem2  33382  nsgqusf1olem3  33383