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 ) |
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 ) |