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. = ( 0g ` G )
triv1nsgd.3
|- ( ph -> G e. Grp )
triv1nsgd.4
|- ( ph -> B = { .0. } )
Assertion triv1nsgd
|- ( ph -> ( NrmSGrp ` G ) ~~ 1o )

Proof

Step Hyp Ref Expression
1 triv1nsgd.1
 |-  B = ( Base ` G )
2 triv1nsgd.2
 |-  .0. = ( 0g ` G )
3 triv1nsgd.3
 |-  ( ph -> G e. Grp )
4 triv1nsgd.4
 |-  ( ph -> B = { .0. } )
5 1 2 3 4 trivnsgd
 |-  ( ph -> ( NrmSGrp ` G ) = { B } )
6 snex
 |-  { .0. } e. _V
7 4 6 eqeltrdi
 |-  ( ph -> B e. _V )
8 ensn1g
 |-  ( B e. _V -> { B } ~~ 1o )
9 7 8 syl
 |-  ( ph -> { B } ~~ 1o )
10 5 9 eqbrtrd
 |-  ( ph -> ( NrmSGrp ` G ) ~~ 1o )