trivnsgd

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

Step	Hyp	Ref	Expression
1		trivnsgd.1	$⊢ B = {Base}_{G}$
2		trivnsgd.2	$⊢ \underset{˙}{0} = 0_{G}$
3		trivnsgd.3	$⊢ φ \to G \in Grp$
4		trivnsgd.4	$⊢ φ \to B = \{\underset{˙}{0}\}$
5		nsgsubg	$⊢ x \in NrmSGrp (G) \to x \in SubGrp (G)$
6	5	a1i	$⊢ φ \to (x \in NrmSGrp (G) \to x \in SubGrp (G))$
7	6	ssrdv	$⊢ φ \to NrmSGrp (G) \subseteq SubGrp (G)$
8	1 2 3 4	trivsubgsnd	$⊢ φ \to SubGrp (G) = \{B\}$
9	7 8	sseqtrd	$⊢ φ \to NrmSGrp (G) \subseteq \{B\}$
10	1	nsgid	$⊢ G \in Grp \to B \in NrmSGrp (G)$
11	3 10	syl	$⊢ φ \to B \in NrmSGrp (G)$
12	11	snssd	$⊢ φ \to \{B\} \subseteq NrmSGrp (G)$
13	9 12	eqssd	$⊢ φ \to NrmSGrp (G) = \{B\}$

Metamath Proof Explorer