Theorem subgrcl 19149

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

Syntax hints:   → wi 4   ∈ wcel 2136   ⊆ wss 3899  ‘cfv 6510  (class class class)co 7385  Basecbs 17221   ↾_s cress 17242  Grpcgrp 18951  SubGrpcsubg 19138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6512  df-fv 6518  df-ov 7388  df-subg 19141

This theorem is referenced by:  subg0  19150  subginv  19151  subgmulgcl  19157  subgsubm  19166  subsubg  19167  subgint  19168  isnsg  19172  nsgconj  19176  isnsg3  19177  ssnmz  19183  nmznsg  19185  eqger  19195  eqgid  19197  eqgen  19198  eqgcpbl  19199  qusgrp  19203  quseccl  19204  qusadd  19205  qus0  19206  qusinv  19207  qussub  19208  ecqusaddcl  19210  resghm2  19249  resghm2b  19250  conjsubg  19266  conjsubgen  19267  conjnmz  19268  conjnmzb  19269  qusghm  19271  ghmqusnsg  19298  ghmquskerlem3  19302  subgga  19316  gastacos  19326  orbstafun  19327  cntrsubgnsg  19359  oppgsubg  19379  isslw  19624  sylow2blem1  19636  sylow2blem2  19637  sylow2blem3  19638  slwhash  19640  lsmval  19664  lsmelval  19665  lsmelvali  19666  lsmelvalm  19667  lsmsubg  19670  lsmless1  19676  lsmless2  19677  lsmless12  19678  lsmass  19685  lsm01  19687  lsm02  19688  subglsm  19689  lsmmod  19691  lsmcntz  19695  lsmcntzr  19696  lsmdisj2  19698  subgdisj1  19707  pj1f  19713  pj1id  19715  pj1lid  19717  pj1rid  19718  pj1ghm  19719  subgdmdprd  20052  subgdprd  20053  dprdsn  20054  pgpfaclem2  20100  cldsubg  24144  gsumsubg  33180  qusker  33489  grplsmid  33544  quslsm  33545  qus0g  33547  qusrn  33549  nsgqus0  33550  nsgmgclem  33551  nsgqusf1olem1  33553  nsgqusf1olem2  33554  nsgqusf1olem3  33555