Theorem subgrcl 19260

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902  ‘cfv 6537  (class class class)co 7417  Basecbs 17307   ↾_s cress 17328  Grpcgrp 19063  SubGrpcsubg 19249

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-subg 19252

This theorem is used by:  subg0  19261  subginv  19262  subgmulgcl  19269  subgsubm  19278  subsubg  19279  subgint  19280  isnsg  19284  nsgconj  19288  isnsg3  19289  ssnmz  19295  nmznsg  19297  eqger  19309  eqgid  19311  eqgen  19312  eqgcpbl  19313  qusgrp  19320  quseccl  19321  qusadd  19322  qus0  19323  qusinv  19324  qussub  19325  ecqusaddcl  19327  resghm2  19366  resghm2b  19367  conjsubg  19383  conjsubgen  19384  conjnmz  19385  conjnmzb  19386  qusghm  19388  ghmqusnsg  19415  ghmquskerlem3  19419  subgga  19433  gastacos  19443  orbstafun  19444  cntrsubgnsg  19476  oppgsubg  19496  isslw  19741  sylow2blem1  19753  sylow2blem2  19754  sylow2blem3  19755  slwhash  19757  lsmval  19781  lsmelval  19782  lsmelvali  19783  lsmelvalm  19784  lsmsubg  19787  lsmless1  19793  lsmless2  19794  lsmless12  19795  lsmass  19802  lsm01  19804  lsm02  19805  subglsm  19806  lsmmod  19808  lsmcntz  19812  lsmcntzr  19813  lsmdisj2  19815  subgdisj1  19824  pj1f  19830  pj1id  19832  pj1lid  19834  pj1rid  19835  pj1ghm  19836  subgdmdprd  20169  subgdprd  20170  dprdsn  20171  pgpfaclem2  20217  cldsubg  24343  gsumsubg  33494  qusker  33797  grplsmid  33841  quslsm  33842  qus0g  33844  qusrn  33846  nsgqus0  33847  nsgmgclem  33848  nsgqusf1olem1  33850  nsgqusf1olem2  33851  nsgqusf1olem3  33852