![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subgrcl | Structured version Visualization version GIF version |
Description: Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
subgrcl | ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2725 | . . 3 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
2 | 1 | issubg 19089 | . 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
3 | 2 | simp1bi 1142 | 1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ⊆ wss 3944 ‘cfv 6549 (class class class)co 7419 Basecbs 17183 ↾s cress 17212 Grpcgrp 18898 SubGrpcsubg 19083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fun 6551 df-fv 6557 df-ov 7422 df-subg 19086 |
This theorem is referenced by: subg0 19095 subginv 19096 subgmulgcl 19102 subgsubm 19111 subsubg 19112 subgint 19113 isnsg 19118 nsgconj 19122 isnsg3 19123 ssnmz 19129 nmznsg 19131 eqger 19141 eqgid 19143 eqgen 19144 eqgcpbl 19145 qusgrp 19149 quseccl 19150 qusadd 19151 qus0 19152 qusinv 19153 qussub 19154 ecqusaddcl 19156 resghm2 19196 resghm2b 19197 conjsubg 19213 conjsubgen 19214 conjnmz 19215 conjnmzb 19216 qusghm 19218 ghmqusnsg 19245 ghmquskerlem3 19249 subgga 19263 gastacos 19273 orbstafun 19274 cntrsubgnsg 19306 oppgsubg 19329 isslw 19575 sylow2blem1 19587 sylow2blem2 19588 sylow2blem3 19589 slwhash 19591 lsmval 19615 lsmelval 19616 lsmelvali 19617 lsmelvalm 19618 lsmsubg 19621 lsmless1 19627 lsmless2 19628 lsmless12 19629 lsmass 19636 lsm01 19638 lsm02 19639 subglsm 19640 lsmmod 19642 lsmcntz 19646 lsmcntzr 19647 lsmdisj2 19649 subgdisj1 19658 pj1f 19664 pj1id 19666 pj1lid 19668 pj1rid 19669 pj1ghm 19670 subgdmdprd 20003 subgdprd 20004 dprdsn 20005 pgpfaclem2 20051 cldsubg 24059 gsumsubg 32850 qusker 33160 grplsmid 33216 quslsm 33217 qus0g 33219 qusrn 33221 nsgqus0 33222 nsgmgclem 33223 nsgqusf1olem1 33225 nsgqusf1olem2 33226 nsgqusf1olem3 33227 |
Copyright terms: Public domain | W3C validator |