Theorem subgrcl 19370

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  ‘cfv 6558  (class class class)co 7443  Basecbs 17416   ↾_s cress 17437  Grpcgrp 19173  SubGrpcsubg 19359

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fv 6566  df-ov 7446  df-subg 19362

This theorem is used by:  subg0  19371  subginv  19372  subgmulgcl  19379  subgsubm  19388  subsubg  19389  subgint  19390  isnsg  19394  nsgconj  19398  isnsg3  19399  ssnmz  19405  nmznsg  19407  eqger  19419  eqgid  19421  eqgen  19422  eqgcpbl  19423  qusgrp  19430  quseccl  19431  qusadd  19432  qus0  19433  qusinv  19434  qussub  19435  ecqusaddcl  19437  resghm2  19476  resghm2b  19477  conjsubg  19493  conjsubgen  19494  conjnmz  19495  conjnmzb  19496  qusghm  19498  ghmqusnsg  19526  ghmquskerlem3  19530  subgga  19544  gastacos  19554  orbstafun  19555  cntrsubgnsg  19587  oppgsubg  19607  isslw  19852  sylow2blem1  19864  sylow2blem2  19865  sylow2blem3  19866  slwhash  19868  lsmval  19892  lsmelval  19893  lsmelvali  19894  lsmelvalm  19895  lsmsubg  19898  lsmless1  19904  lsmless2  19905  lsmless12  19906  lsmass  19913  lsm01  19915  lsm02  19916  subglsm  19917  lsmmod  19919  lsmcntz  19923  lsmcntzr  19924  lsmdisj2  19926  subgdisj1  19935  pj1f  19941  pj1id  19943  pj1lid  19945  pj1rid  19946  pj1ghm  19947  subgdmdprd  20280  subgdprd  20281  dprdsn  20282  pgpfaclem2  20328  cldsubg  24460  gsumsubg  33677  qusker  33980  grplsmid  34025  quslsm  34026  qus0g  34028  qusrn  34030  nsgqus0  34031  nsgmgclem  34032  nsgqusf1olem1  34034  nsgqusf1olem2  34035  nsgqusf1olem3  34036