Metamath Proof Explorer

Theorem 2nsgsimpgd

Description: If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 2nsgsimpgd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 2nsgsimpgd.2
3 2nsgsimpgd.3 ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
4 2nsgsimpgd.4
5 2nsgsimpgd.5
6 elprg
8 5 7 mpbird
9 simpr
10 2 0nsg
11 3 10 syl
13 9 12 eqeltrd
15 simpr ${⊢}\left({\phi }\wedge {x}={B}\right)\to {x}={B}$
16 1 nsgid ${⊢}{G}\in \mathrm{Grp}\to {B}\in \mathrm{NrmSGrp}\left({G}\right)$
17 3 16 syl ${⊢}{\phi }\to {B}\in \mathrm{NrmSGrp}\left({G}\right)$
18 17 adantr ${⊢}\left({\phi }\wedge {x}={B}\right)\to {B}\in \mathrm{NrmSGrp}\left({G}\right)$
19 15 18 eqeltrd ${⊢}\left({\phi }\wedge {x}={B}\right)\to {x}\in \mathrm{NrmSGrp}\left({G}\right)$
28 1 fvexi ${⊢}{B}\in \mathrm{V}$
29 28 a1i ${⊢}{\phi }\to {B}\in \mathrm{V}$
31 25 30 eqbrtrd ${⊢}{\phi }\to \mathrm{NrmSGrp}\left({G}\right)\approx {2}_{𝑜}$
32 3 31 issimpgd ${⊢}{\phi }\to {G}\in \mathrm{SimpGrp}$