Theorem triv1nsgd

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

	Ref	Expression
Hypotheses	triv1nsgd.1	$$⊢B={\mathrm{Base}}_G$$
	triv1nsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	triv1nsgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
	triv1nsgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	triv1nsgd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		triv1nsgd.1	$$⊢B={\mathrm{Base}}_G$$
2		triv1nsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		triv1nsgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		triv1nsgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
5	1 2 3 4	trivnsgd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{B\right\}$$
6		snex	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
7	4 6	eqeltrdi	$$⊢\phi \to B\in \mathrm{V}$$
8		ensn1g	$$⊢B\in \mathrm{V}\to \left\{B\right\}\approx 1_{𝑜}$$
9	7 8	syl	$$⊢\phi \to \left\{B\right\}\approx 1_{𝑜}$$
10	5 9	eqbrtrd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\approx 1_{𝑜}$$