Definition df-simpg 19478

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.)

Assertion

Ref	Expression
df-simpg	⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o}

Detailed syntax breakdown of Definition df-simpg

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}

This definition is referenced by:  issimpg  19479