Theorem subgrcl 18827

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3896  ‘cfv 6463  (class class class)co 7313  Basecbs 16979   ↾_s cress 17008  Grpcgrp 18644  SubGrpcsubg 18816

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-iota 6415  df-fun 6465  df-fv 6471  df-ov 7316  df-subg 18819

This theorem is referenced by:  subg0  18828  subginv  18829  subgmulgcl  18835  subgsubm  18844  subsubg  18845  subgint  18846  isnsg  18850  nsgconj  18854  isnsg3  18855  ssnmz  18861  nmznsg  18863  eqger  18873  eqgid  18875  eqgen  18876  eqgcpbl  18877  qusgrp  18878  quseccl  18879  qusadd  18880  qus0  18881  qusinv  18882  qussub  18883  resghm2  18918  resghm2b  18919  conjsubg  18933  conjsubgen  18934  conjnmz  18935  conjnmzb  18936  qusghm  18938  subgga  18973  gastacos  18983  orbstafun  18984  cntrsubgnsg  19014  oppgsubg  19037  isslw  19280  sylow2blem1  19292  sylow2blem2  19293  sylow2blem3  19294  slwhash  19296  lsmval  19320  lsmelval  19321  lsmelvali  19322  lsmelvalm  19323  lsmsubg  19326  lsmless1  19332  lsmless2  19333  lsmless12  19334  lsmass  19342  lsm01  19344  lsm02  19345  subglsm  19346  lsmmod  19348  lsmcntz  19352  lsmcntzr  19353  lsmdisj2  19355  subgdisj1  19364  pj1f  19370  pj1id  19372  pj1lid  19374  pj1rid  19375  pj1ghm  19376  subgdmdprd  19704  subgdprd  19705  dprdsn  19706  pgpfaclem2  19752  cldsubg  23333  gsumsubg  31414  qusker  31653  grplsmid  31697  quslsm  31698  nsgqus0  31700  nsgmgclem  31701  nsgqusf1olem1  31703  nsgqusf1olem2  31704  nsgqusf1olem3  31705