![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-simpg | Structured version Visualization version GIF version |
Description: Define class of all simple groups. A simple group is a group (df-grp 18711) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 19841). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Ref | Expression |
---|---|
df-simpg | ⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csimpg 19828 | . 2 class SimpGrp | |
2 | vg | . . . . . 6 setvar 𝑔 | |
3 | 2 | cv 1540 | . . . . 5 class 𝑔 |
4 | cnsg 18882 | . . . . 5 class NrmSGrp | |
5 | 3, 4 | cfv 6493 | . . . 4 class (NrmSGrp‘𝑔) |
6 | c2o 8398 | . . . 4 class 2o | |
7 | cen 8838 | . . . 4 class ≈ | |
8 | 5, 6, 7 | wbr 5103 | . . 3 wff (NrmSGrp‘𝑔) ≈ 2o |
9 | cgrp 18708 | . . 3 class Grp | |
10 | 8, 2, 9 | crab 3405 | . 2 class {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} |
11 | 1, 10 | wceq 1541 | 1 wff SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} |
Colors of variables: wff setvar class |
This definition is referenced by: issimpg 19830 |
Copyright terms: Public domain | W3C validator |