Theorem subgrcl 19228

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3908  ‘cfv 6543  (class class class)co 7423  Basecbs 17294   ↾_s cress 17315  Grpcgrp 19031  SubGrpcsubg 19217

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-subg 19220

This theorem is used by:  subg0  19229  subginv  19230  subgmulgcl  19237  subgsubm  19246  subsubg  19247  subgint  19248  isnsg  19252  nsgconj  19256  isnsg3  19257  ssnmz  19263  nmznsg  19265  eqger  19277  eqgid  19279  eqgen  19280  eqgcpbl  19281  qusgrp  19288  quseccl  19289  qusadd  19290  qus0  19291  qusinv  19292  qussub  19293  ecqusaddcl  19295  resghm2  19334  resghm2b  19335  conjsubg  19351  conjsubgen  19352  conjnmz  19353  conjnmzb  19354  qusghm  19356  ghmqusnsg  19383  ghmquskerlem3  19387  subgga  19401  gastacos  19411  orbstafun  19412  cntrsubgnsg  19444  oppgsubg  19464  isslw  19709  sylow2blem1  19721  sylow2blem2  19722  sylow2blem3  19723  slwhash  19725  lsmval  19749  lsmelval  19750  lsmelvali  19751  lsmelvalm  19752  lsmsubg  19755  lsmless1  19761  lsmless2  19762  lsmless12  19763  lsmass  19770  lsm01  19772  lsm02  19773  subglsm  19774  lsmmod  19776  lsmcntz  19780  lsmcntzr  19781  lsmdisj2  19783  subgdisj1  19792  pj1f  19798  pj1id  19800  pj1lid  19802  pj1rid  19803  pj1ghm  19804  subgdmdprd  20137  subgdprd  20138  dprdsn  20139  pgpfaclem2  20185  cldsubg  24305  gsumsubg  33397  qusker  33700  grplsmid  33744  quslsm  33745  qus0g  33747  qusrn  33749  nsgqus0  33750  nsgmgclem  33751  nsgqusf1olem1  33753  nsgqusf1olem2  33754  nsgqusf1olem3  33755