Theorem subgrcl 19044

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902  ‘cfv 6481  (class class class)co 7346  Basecbs 17120   ↾_s cress 17141  Grpcgrp 18846  SubGrpcsubg 19033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-subg 19036

This theorem is referenced by:  subg0  19045  subginv  19046  subgmulgcl  19052  subgsubm  19061  subsubg  19062  subgint  19063  isnsg  19068  nsgconj  19072  isnsg3  19073  ssnmz  19079  nmznsg  19081  eqger  19091  eqgid  19093  eqgen  19094  eqgcpbl  19095  qusgrp  19099  quseccl  19100  qusadd  19101  qus0  19102  qusinv  19103  qussub  19104  ecqusaddcl  19106  resghm2  19146  resghm2b  19147  conjsubg  19163  conjsubgen  19164  conjnmz  19165  conjnmzb  19166  qusghm  19168  ghmqusnsg  19195  ghmquskerlem3  19199  subgga  19213  gastacos  19223  orbstafun  19224  cntrsubgnsg  19256  oppgsubg  19276  isslw  19521  sylow2blem1  19533  sylow2blem2  19534  sylow2blem3  19535  slwhash  19537  lsmval  19561  lsmelval  19562  lsmelvali  19563  lsmelvalm  19564  lsmsubg  19567  lsmless1  19573  lsmless2  19574  lsmless12  19575  lsmass  19582  lsm01  19584  lsm02  19585  subglsm  19586  lsmmod  19588  lsmcntz  19592  lsmcntzr  19593  lsmdisj2  19595  subgdisj1  19604  pj1f  19610  pj1id  19612  pj1lid  19614  pj1rid  19615  pj1ghm  19616  subgdmdprd  19949  subgdprd  19950  dprdsn  19951  pgpfaclem2  19997  cldsubg  24027  gsumsubg  33024  qusker  33312  grplsmid  33367  quslsm  33368  qus0g  33370  qusrn  33372  nsgqus0  33373  nsgmgclem  33374  nsgqusf1olem1  33376  nsgqusf1olem2  33377  nsgqusf1olem3  33378