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 18368) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 19490). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Ref | Expression |
---|---|
df-simpg | ⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csimpg 19477 | . 2 class SimpGrp | |
2 | vg | . . . . . 6 setvar 𝑔 | |
3 | 2 | cv 1542 | . . . . 5 class 𝑔 |
4 | cnsg 18538 | . . . . 5 class NrmSGrp | |
5 | 3, 4 | cfv 6380 | . . . 4 class (NrmSGrp‘𝑔) |
6 | c2o 8196 | . . . 4 class 2o | |
7 | cen 8623 | . . . 4 class ≈ | |
8 | 5, 6, 7 | wbr 5053 | . . 3 wff (NrmSGrp‘𝑔) ≈ 2o |
9 | cgrp 18365 | . . 3 class Grp | |
10 | 8, 2, 9 | crab 3065 | . 2 class {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} |
11 | 1, 10 | wceq 1543 | 1 wff SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} |
Colors of variables: wff setvar class |
This definition is referenced by: issimpg 19479 |
Copyright terms: Public domain | W3C validator |