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	$$⊢\mathrm{SimpGrp}=\left\{g\in \mathrm{Grp}|\mathrm{NrmSGrp}\left(g\right)\approx 2_{𝑜}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csimpg	$$class\mathrm{SimpGrp}$$
1		vg	$$setvarg$$
2		cgrp	$$class\mathrm{Grp}$$
3		cnsg	$$class\mathrm{NrmSGrp}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class\mathrm{NrmSGrp}\left(g\right)$$
6		cen	$$class\approx$$
7		c2o	$$class{2}_{𝑜}$$
8	5 7 6	wbr	$$wff\mathrm{NrmSGrp}\left(g\right)\approx 2_{𝑜}$$
9	8 1 2	crab	$$class\left\{g\in \mathrm{Grp}|\mathrm{NrmSGrp}\left(g\right)\approx 2_{𝑜}\right\}$$
10	0 9	wceq	$$wff\mathrm{SimpGrp}=\left\{g\in \mathrm{Grp}|\mathrm{NrmSGrp}\left(g\right)\approx 2_{𝑜}\right\}$$