Theorem 0idnsgd

Description: The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		0idnsgd.1	|- B = ( Base ` G )
2		0idnsgd.2	|- .0. = ( 0g ` G )
3		0idnsgd.3	|- ( ph -> G e. Grp )
4	2	0nsg	|- ( G e. Grp -> { .0. } e. ( NrmSGrp ` G ) )
5	3 4	syl	|- ( ph -> { .0. } e. ( NrmSGrp ` G ) )
6	1	nsgid	|- ( G e. Grp -> B e. ( NrmSGrp ` G ) )
7	3 6	syl	|- ( ph -> B e. ( NrmSGrp ` G ) )
8	5 7	prssd	|- ( ph -> { { .0. } , B } C_ ( NrmSGrp ` G ) )