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

Metamath Proof Explorer

Theorem trivnsgd

Description: The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses trivnsgd.1 
|- B = ( Base ` G )
trivnsgd.2 
|- .0. = ( 0g ` G )
trivnsgd.3 
|- ( ph -> G e. Grp )
trivnsgd.4 
|- ( ph -> B = { .0. } )
Assertion trivnsgd 
|- ( ph -> ( NrmSGrp ` G ) = { B } )

Proof

Step Hyp Ref Expression
1 trivnsgd.1 
 |-  B = ( Base ` G )
2 trivnsgd.2 
 |-  .0. = ( 0g ` G )
3 trivnsgd.3 
 |-  ( ph -> G e. Grp )
4 trivnsgd.4 
 |-  ( ph -> B = { .0. } )
5 nsgsubg 
 |-  ( x e. ( NrmSGrp ` G ) -> x e. ( SubGrp ` G ) )
6 5 a1i 
 |-  ( ph -> ( x e. ( NrmSGrp ` G ) -> x e. ( SubGrp ` G ) ) )
7 6 ssrdv 
 |-  ( ph -> ( NrmSGrp ` G ) C_ ( SubGrp ` G ) )
8 1 2 3 4 trivsubgsnd 
 |-  ( ph -> ( SubGrp ` G ) = { B } )
9 7 8 sseqtrd 
 |-  ( ph -> ( NrmSGrp ` G ) C_ { B } )
10 1 nsgid 
 |-  ( G e. Grp -> B e. ( NrmSGrp ` G ) )
11 3 10 syl 
 |-  ( ph -> B e. ( NrmSGrp ` G ) )
12 11 snssd 
 |-  ( ph -> { B } C_ ( NrmSGrp ` G ) )
13 9 12 eqssd 
 |-  ( ph -> ( NrmSGrp ` G ) = { B } )