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 B = Base G
triv1nsgd.2 0 ˙ = 0 G
triv1nsgd.3 φ G Grp
triv1nsgd.4 φ B = 0 ˙
Assertion triv1nsgd φ NrmSGrp G 1 𝑜

Proof

Step Hyp Ref Expression
1 triv1nsgd.1 B = Base G
2 triv1nsgd.2 0 ˙ = 0 G
3 triv1nsgd.3 φ G Grp
4 triv1nsgd.4 φ B = 0 ˙
5 1 2 3 4 trivnsgd φ NrmSGrp G = B
6 snex 0 ˙ V
7 4 6 eqeltrdi φ B V
8 ensn1g B V B 1 𝑜
9 7 8 syl φ B 1 𝑜
10 5 9 eqbrtrd φ NrmSGrp G 1 𝑜