Theorem trivsubgd

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

	Ref	Expression
Hypotheses	trivsubgd.1	$$⊢B={\mathrm{Base}}_G$$
	trivsubgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	trivsubgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
	trivsubgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
	trivsubgd.5	$$⊢\phi \to A\in \mathrm{SubGrp}\left(G\right)$$
Assertion	trivsubgd	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		trivsubgd.1	$$⊢B={\mathrm{Base}}_G$$
2		trivsubgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		trivsubgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		trivsubgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
5		trivsubgd.5	$$⊢\phi \to A\in \mathrm{SubGrp}\left(G\right)$$
6	1	subgss	$$⊢A\in \mathrm{SubGrp}\left(G\right)\to A\subseteq B$$
7	5 6	syl	$$⊢\phi \to A\subseteq B$$
8	7 4	sseqtrd	$$⊢\phi \to A\subseteq \left\{\underset{\dot{}}{0}\right\}$$
9	2	subg0cl	$$⊢A\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in A$$
10	5 9	syl	$$⊢\phi \to \underset{\dot{}}{0}\in A$$
11	10	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq A$$
12	8 11	eqssd	$$⊢\phi \to A=\left\{\underset{\dot{}}{0}\right\}$$
13	12 4	eqtr4d	$$⊢\phi \to A=B$$