![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > grpbn0 | Structured version Visualization version GIF version |
Description: The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
Ref | Expression |
---|---|
grpbn0.b | ⊢ 𝐵 = (Base‘𝐺) |
Ref | Expression |
---|---|
grpbn0 | ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpbn0.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
2 | eqid 2752 | . . 3 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
3 | 1, 2 | grpidcl 17643 | . 2 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ 𝐵) |
4 | ne0i 4056 | . 2 ⊢ ((0g‘𝐺) ∈ 𝐵 → 𝐵 ≠ ∅) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1624 ∈ wcel 2131 ≠ wne 2924 ∅c0 4050 ‘cfv 6041 Basecbs 16051 0gc0g 16294 Grpcgrp 17615 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-reu 3049 df-rmo 3050 df-rab 3051 df-v 3334 df-sbc 3569 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-iota 6004 df-fun 6043 df-fv 6049 df-riota 6766 df-ov 6808 df-0g 16296 df-mgm 17435 df-sgrp 17477 df-mnd 17488 df-grp 17618 |
This theorem is referenced by: grpn0 17647 dfgrp3 17707 issubg2 17802 grpissubg 17807 ghmrn 17866 gexcl3 18194 gexcl2 18196 sylow1lem1 18205 sylow1lem3 18207 sylow1lem5 18209 pgpfi 18212 pgpfi2 18213 sylow2blem3 18229 slwhash 18231 fislw 18232 gexex 18448 lt6abl 18488 ablfac1lem 18659 ablfac1b 18661 ablfac1c 18662 ablfac1eu 18664 pgpfac1lem2 18666 pgpfac1lem3a 18667 ablfaclem3 18678 dvdsr02 18848 lmodbn0 19067 lmodsn0 19070 rmodislmodlem 19124 rmodislmod 19125 islss3 19153 0ringnnzr 19463 isclmp 23089 dfacbasgrp 38172 |
Copyright terms: Public domain | W3C validator |