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 )