Theorem trivsubgsnd

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

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

Proof

Step	Hyp	Ref	Expression
1		trivsubgsnd.1	$$⊢B={\mathrm{Base}}_G$$
2		trivsubgsnd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		trivsubgsnd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		trivsubgsnd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
5	3	adantr	$$⊢\left(\phi \wedge x\in \mathrm{SubGrp}\left(G\right)\right)\to G\in \mathrm{Grp}$$
6	4	adantr	$$⊢\left(\phi \wedge x\in \mathrm{SubGrp}\left(G\right)\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
7		simpr	$$⊢\left(\phi \wedge x\in \mathrm{SubGrp}\left(G\right)\right)\to x\in \mathrm{SubGrp}\left(G\right)$$
8	1 2 5 6 7	trivsubgd	$$⊢\left(\phi \wedge x\in \mathrm{SubGrp}\left(G\right)\right)\to x=B$$
9		velsn	$$⊢x\in \left\{B\right\}\leftrightarrow x=B$$
10	8 9	sylibr	$$⊢\left(\phi \wedge x\in \mathrm{SubGrp}\left(G\right)\right)\to x\in \left\{B\right\}$$
11	10	ex	$$⊢\phi \to \left(x\in \mathrm{SubGrp}\left(G\right)\to x\in \left\{B\right\}\right)$$
12	11	ssrdv	$$⊢\phi \to \mathrm{SubGrp}\left(G\right)\subseteq \left\{B\right\}$$
13	1	subgid	$$⊢G\in \mathrm{Grp}\to B\in \mathrm{SubGrp}\left(G\right)$$
14	3 13	syl	$$⊢\phi \to B\in \mathrm{SubGrp}\left(G\right)$$
15	14	snssd	$$⊢\phi \to \left\{B\right\}\subseteq \mathrm{SubGrp}\left(G\right)$$
16	12 15	eqssd	$$⊢\phi \to \mathrm{SubGrp}\left(G\right)=\left\{B\right\}$$