1nsgtrivd

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

Step	Hyp	Ref	Expression
1		1nsgtrivd.1	$⊢ B = {Base}_{G}$
2		1nsgtrivd.2	$⊢ \underset{˙}{0} = 0_{G}$
3		1nsgtrivd.3	$⊢ φ \to G \in Grp$
4		1nsgtrivd.4	$⊢ φ \to NrmSGrp (G) \approx 1_{𝑜}$
5	1	nsgid	$⊢ G \in Grp \to B \in NrmSGrp (G)$
6	3 5	syl	$⊢ φ \to B \in NrmSGrp (G)$
7	2	0nsg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in NrmSGrp (G)$
8	3 7	syl	$⊢ φ \to \{\underset{˙}{0}\} \in NrmSGrp (G)$
9		en1eqsn	$⊢ (\{\underset{˙}{0}\} \in NrmSGrp (G) \land NrmSGrp (G) \approx 1_{𝑜}) \to NrmSGrp (G) = \{\{\underset{˙}{0}\}\}$
10	8 4 9	syl2anc	$⊢ φ \to NrmSGrp (G) = \{\{\underset{˙}{0}\}\}$
11	6 10	eleqtrd	$⊢ φ \to B \in \{\{\underset{˙}{0}\}\}$
12		snex	$⊢ \{\underset{˙}{0}\} \in V$
13		elsn2g	$⊢ \{\underset{˙}{0}\} \in V \to (B \in \{\{\underset{˙}{0}\}\} \leftrightarrow B = \{\underset{˙}{0}\})$
14	12 13	mp1i	$⊢ φ \to (B \in \{\{\underset{˙}{0}\}\} \leftrightarrow B = \{\underset{˙}{0}\})$
15	11 14	mpbid	$⊢ φ \to B = \{\underset{˙}{0}\}$

Metamath Proof Explorer