trivsubgsnd

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

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

Metamath Proof Explorer