Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-simpg Structured version   Visualization version   GIF version

Definition df-simpg 19227
 Description: Define class of all simple groups. A simple group is a group (df-grp 18118) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 19239). (Contributed by Rohan Ridenour, 3-Aug-2023.)
Assertion
Ref Expression
df-simpg SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}

Detailed syntax breakdown of Definition df-simpg
StepHypRef Expression
1 csimpg 19226 . 2 class SimpGrp
2 vg . . . . . 6 setvar 𝑔
32cv 1537 . . . . 5 class 𝑔
4 cnsg 18287 . . . . 5 class NrmSGrp
53, 4cfv 6332 . . . 4 class (NrmSGrp‘𝑔)
6 c2o 8097 . . . 4 class 2o
7 cen 8507 . . . 4 class
85, 6, 7wbr 5034 . . 3 wff (NrmSGrp‘𝑔) ≈ 2o
9 cgrp 18115 . . 3 class Grp
108, 2, 9crab 3110 . 2 class {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
111, 10wceq 1538 1 wff SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}
 Colors of variables: wff setvar class This definition is referenced by:  issimpg  19228
 Copyright terms: Public domain W3C validator