Theorem triv1nsgd

Description: A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	triv1nsgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	triv1nsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	triv1nsgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	triv1nsgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
Assertion	triv1nsgd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ 1o )

Proof

Step	Hyp	Ref	Expression
1		triv1nsgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		triv1nsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		triv1nsgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		triv1nsgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
5	1 2 3 4	trivnsgd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { 𝐵 } )
6		snex	⊢ { 0 } ∈ V
7	4 6	eqeltrdi	⊢ ( 𝜑 → 𝐵 ∈ V )
8		ensn1g	⊢ ( 𝐵 ∈ V → { 𝐵 } ≈ 1o )
9	7 8	syl	⊢ ( 𝜑 → { 𝐵 } ≈ 1o )
10	5 9	eqbrtrd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ 1o )