Theorem 1nsgtrivd

Description: A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		1nsgtrivd.1	|- B = ( Base ` G )
2		1nsgtrivd.2	|- .0. = ( 0g ` G )
3		1nsgtrivd.3	|- ( ph -> G e. Grp )
4		1nsgtrivd.4	|- ( ph -> ( NrmSGrp ` G ) ~~ 1o )
5	1	nsgid	|- ( G e. Grp -> B e. ( NrmSGrp ` G ) )
6	3 5	syl	|- ( ph -> B e. ( NrmSGrp ` G ) )
7	2	0nsg	|- ( G e. Grp -> { .0. } e. ( NrmSGrp ` G ) )
8	3 7	syl	|- ( ph -> { .0. } e. ( NrmSGrp ` G ) )
9		en1eqsn	|- ( ( { .0. } e. ( NrmSGrp ` G ) /\ ( NrmSGrp ` G ) ~~ 1o ) -> ( NrmSGrp ` G ) = { { .0. } } )
10	8 4 9	syl2anc	|- ( ph -> ( NrmSGrp ` G ) = { { .0. } } )
11	6 10	eleqtrd	|- ( ph -> B e. { { .0. } } )
12		snex	|- { .0. } e. _V
13		elsn2g	|- ( { .0. } e. _V -> ( B e. { { .0. } } <-> B = { .0. } ) )
14	12 13	mp1i	|- ( ph -> ( B e. { { .0. } } <-> B = { .0. } ) )
15	11 14	mpbid	|- ( ph -> B = { .0. } )