Definition df-simpg

Description: Define class of all simple groups. A simple group is a group ( df-grp ) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity ( simpgnsgbid ). (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Assertion	df-simpg	|- SimpGrp = { g e. Grp | ( NrmSGrp ` g ) ~~ 2o }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csimpg	|- SimpGrp
1		vg	|- g
2		cgrp	|- Grp
3		cnsg	|- NrmSGrp
4	1	cv	|- g
5	4 3	cfv	|- ( NrmSGrp ` g )
6		cen	|- ~~
7		c2o	|- 2o
8	5 7 6	wbr	|- ( NrmSGrp ` g ) ~~ 2o
9	8 1 2	crab	|- { g e. Grp | ( NrmSGrp ` g ) ~~ 2o }
10	0 9	wceq	|- SimpGrp = { g e. Grp | ( NrmSGrp ` g ) ~~ 2o }