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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	2nsgsimpgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	2nsgsimpgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	2nsgsimpgd.4	⊢ ( 𝜑 → ¬ { 0 } = 𝐵 )
	2nsgsimpgd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) )
Assertion	2nsgsimpgd	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )

Proof

Step	Hyp	Ref	Expression
1		2nsgsimpgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		2nsgsimpgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		2nsgsimpgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		2nsgsimpgd.4	⊢ ( 𝜑 → ¬ { 0 } = 𝐵 )
5		2nsgsimpgd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) )
6		elprg	⊢ ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝑥 ∈ { { 0 } , 𝐵 } ↔ ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ { { 0 } , 𝐵 } ↔ ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) ) )
8	5 7	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝑥 ∈ { { 0 } , 𝐵 } )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = { 0 } ) → 𝑥 = { 0 } )
10	2	0nsg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
11	3 10	syl	⊢ ( 𝜑 → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = { 0 } ) → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
13	9 12	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 = { 0 } ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) )
14	13	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { { 0 } , 𝐵 } ) ∧ 𝑥 = { 0 } ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
16	1	nsgid	⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
17	3 16	syl	⊢ ( 𝜑 → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
19	15 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) )
20	19	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { { 0 } , 𝐵 } ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) )
21		elpri	⊢ ( 𝑥 ∈ { { 0 } , 𝐵 } → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { { 0 } , 𝐵 } ) → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) )
23	14 20 22	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { { 0 } , 𝐵 } ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) )
24	8 23	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑥 ∈ { { 0 } , 𝐵 } ) )
25	24	eqrdv	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } )
26		snex	⊢ { 0 } ∈ V
27	26	a1i	⊢ ( 𝜑 → { 0 } ∈ V )
28	1	fvexi	⊢ 𝐵 ∈ V
29	28	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
30	27 29 4	enpr2d	⊢ ( 𝜑 → { { 0 } , 𝐵 } ≈ 2o )
31	25 30	eqbrtrd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ 2o )
32	3 31	issimpgd	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )