# Metamath Proof Explorer

## 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 ${setvar}{g}$
2 cgrp ${class}\mathrm{Grp}$
3 cnsg ${class}\mathrm{NrmSGrp}$
4 1 cv ${setvar}{g}$
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\}$