# Metamath Proof Explorer

## Theorem simpgnsgd

Description: The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses simpgnsgd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
simpgnsgd.2
simpgnsgd.3 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
Assertion simpgnsgd

### Proof

Step Hyp Ref Expression
1 simpgnsgd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 simpgnsgd.2
3 simpgnsgd.3 ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$
4 2onn ${⊢}{2}_{𝑜}\in \mathrm{\omega }$
5 4 a1i ${⊢}{\phi }\to {2}_{𝑜}\in \mathrm{\omega }$
6 nnfi ${⊢}{2}_{𝑜}\in \mathrm{\omega }\to {2}_{𝑜}\in \mathrm{Fin}$
7 5 6 syl ${⊢}{\phi }\to {2}_{𝑜}\in \mathrm{Fin}$
8 simpg2nsg ${⊢}{G}\in \mathrm{SimpGrp}\to \mathrm{NrmSGrp}\left({G}\right)\approx {2}_{𝑜}$
9 3 8 syl ${⊢}{\phi }\to \mathrm{NrmSGrp}\left({G}\right)\approx {2}_{𝑜}$
10 enfii ${⊢}\left({2}_{𝑜}\in \mathrm{Fin}\wedge \mathrm{NrmSGrp}\left({G}\right)\approx {2}_{𝑜}\right)\to \mathrm{NrmSGrp}\left({G}\right)\in \mathrm{Fin}$
11 7 9 10 syl2anc ${⊢}{\phi }\to \mathrm{NrmSGrp}\left({G}\right)\in \mathrm{Fin}$
12 3 simpggrpd ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
13 1 2 12 0idnsgd
14 snex
15 14 a1i
16 1 a1i ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{G}}$
17 fvex ${⊢}{\mathrm{Base}}_{{G}}\in \mathrm{V}$
18 16 17 eqeltrdi ${⊢}{\phi }\to {B}\in \mathrm{V}$
19 1 2 3 simpgntrivd
20 19 neqcomd
21 15 18 20 enpr2d
22 21 ensymd
23 entr
24 9 22 23 syl2anc
25 11 13 24 phpeqd