Theorem subgrcl 19321

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ‘cfv 6531  (class class class)co 7412  Basecbs 17367   ↾_s cress 17388  Grpcgrp 19124  SubGrpcsubg 19310

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fv 6539  df-ov 7415  df-subg 19313

This theorem is used by:  subg0  19322  subginv  19323  subgmulgcl  19330  subgsubm  19339  subsubg  19340  subgint  19341  isnsg  19345  nsgconj  19349  isnsg3  19350  ssnmz  19356  nmznsg  19358  eqger  19370  eqgid  19372  eqgen  19373  eqgcpbl  19374  qusgrp  19381  quseccl  19382  qusadd  19383  qus0  19384  qusinv  19385  qussub  19386  ecqusaddcl  19388  resghm2  19427  resghm2b  19428  conjsubg  19444  conjsubgen  19445  conjnmz  19446  conjnmzb  19447  qusghm  19449  ghmqusnsg  19476  ghmquskerlem3  19480  subgga  19494  gastacos  19504  orbstafun  19505  cntrsubgnsg  19537  oppgsubg  19557  isslw  19802  sylow2blem1  19814  sylow2blem2  19815  sylow2blem3  19816  slwhash  19818  lsmval  19842  lsmelval  19843  lsmelvali  19844  lsmelvalm  19845  lsmsubg  19848  lsmless1  19854  lsmless2  19855  lsmless12  19856  lsmass  19863  lsm01  19865  lsm02  19866  subglsm  19867  lsmmod  19869  lsmcntz  19873  lsmcntzr  19874  lsmdisj2  19876  subgdisj1  19885  pj1f  19891  pj1id  19893  pj1lid  19895  pj1rid  19896  pj1ghm  19897  subgdmdprd  20230  subgdprd  20231  dprdsn  20232  pgpfaclem2  20278  cldsubg  24410  gsumsubg  33589  qusker  33892  grplsmid  33937  quslsm  33938  qus0g  33940  qusrn  33942  nsgqus0  33943  nsgmgclem  33944  nsgqusf1olem1  33946  nsgqusf1olem2  33947  nsgqusf1olem3  33948