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 = { 𝑔 ∈ Grp ∣ ( NrmSGrp ‘ 𝑔 ) ≈ 2o }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csimpg	⊢ SimpGrp
1		vg	⊢ 𝑔
2		cgrp	⊢ Grp
3		cnsg	⊢ NrmSGrp
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( NrmSGrp ‘ 𝑔 )
6		cen	⊢ ≈
7		c2o	⊢ 2o
8	5 7 6	wbr	⊢ ( NrmSGrp ‘ 𝑔 ) ≈ 2o
9	8 1 2	crab	⊢ { 𝑔 ∈ Grp ∣ ( NrmSGrp ‘ 𝑔 ) ≈ 2o }
10	0 9	wceq	⊢ SimpGrp = { 𝑔 ∈ Grp ∣ ( NrmSGrp ‘ 𝑔 ) ≈ 2o }