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