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	$$⊢\underset{\dot{}}{0}=0_G$$
	simpgnsgd.3	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
Assertion	simpgnsgd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		simpgnsgd.1	$$⊢B={\mathrm{Base}}_G$$
2		simpgnsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
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	$$⊢\phi \to \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\subseteq \mathrm{NrmSGrp}\left(G\right)$$
14		snex	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
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	$$⊢\phi \to \neg B=\left\{\underset{\dot{}}{0}\right\}$$
20	19	neqcomd	$$⊢\phi \to \neg \left\{\underset{\dot{}}{0}\right\}=B$$
21	15 18 20	enpr2d	$$⊢\phi \to \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\approx 2_{𝑜}$$
22	21	ensymd	$$⊢\phi \to 2_{𝑜}\approx \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$
23		entr	$$⊢\left(\mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}\wedge 2_{𝑜}\approx \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\right)\to \mathrm{NrmSGrp}\left(G\right)\approx \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$
24	9 22 23	syl2anc	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\approx \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$
25	11 13 24	phpeqd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$