Metamath Proof Explorer


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 = Base G
trivsubgsnd.2 0 ˙ = 0 G
trivsubgsnd.3 φ G Grp
trivsubgsnd.4 φ B = 0 ˙
Assertion trivsubgsnd φ SubGrp G = B

Proof

Step Hyp Ref Expression
1 trivsubgsnd.1 B = Base G
2 trivsubgsnd.2 0 ˙ = 0 G
3 trivsubgsnd.3 φ G Grp
4 trivsubgsnd.4 φ B = 0 ˙
5 3 adantr φ x SubGrp G G Grp
6 4 adantr φ x SubGrp G B = 0 ˙
7 simpr φ x SubGrp G x SubGrp G
8 1 2 5 6 7 trivsubgd φ x SubGrp G x = B
9 velsn x B x = B
10 8 9 sylibr φ x SubGrp G x B
11 10 ex φ x SubGrp G x B
12 11 ssrdv φ SubGrp G B
13 1 subgid G Grp B SubGrp G
14 3 13 syl φ B SubGrp G
15 14 snssd φ B SubGrp G
16 12 15 eqssd φ SubGrp G = B