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 = ( Base ` G )
	trivsubgd.2	|- .0. = ( 0g ` G )
	trivsubgd.3	|- ( ph -> G e. Grp )
	trivsubgd.4	|- ( ph -> B = { .0. } )
	trivsubgd.5	|- ( ph -> A e. ( SubGrp ` G ) )
Assertion	trivsubgd	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		trivsubgd.1	|- B = ( Base ` G )
2		trivsubgd.2	|- .0. = ( 0g ` G )
3		trivsubgd.3	|- ( ph -> G e. Grp )
4		trivsubgd.4	|- ( ph -> B = { .0. } )
5		trivsubgd.5	|- ( ph -> A e. ( SubGrp ` G ) )
6	1	subgss	|- ( A e. ( SubGrp ` G ) -> A C_ B )
7	5 6	syl	|- ( ph -> A C_ B )
8	7 4	sseqtrd	|- ( ph -> A C_ { .0. } )
9	2	subg0cl	|- ( A e. ( SubGrp ` G ) -> .0. e. A )
10	5 9	syl	|- ( ph -> .0. e. A )
11	10	snssd	|- ( ph -> { .0. } C_ A )
12	8 11	eqssd	|- ( ph -> A = { .0. } )
13	12 4	eqtr4d	|- ( ph -> A = B )