This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )