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

Proof

Step	Hyp	Ref	Expression
1		trivsubgsnd.1	|- B = ( Base ` G )
2		trivsubgsnd.2	|- .0. = ( 0g ` G )
3		trivsubgsnd.3	|- ( ph -> G e. Grp )
4		trivsubgsnd.4	|- ( ph -> B = { .0. } )
5	3	adantr	|- ( ( ph /\ x e. ( SubGrp ` G ) ) -> G e. Grp )
6	4	adantr	|- ( ( ph /\ x e. ( SubGrp ` G ) ) -> B = { .0. } )
7		simpr	|- ( ( ph /\ x e. ( SubGrp ` G ) ) -> x e. ( SubGrp ` G ) )
8	1 2 5 6 7	trivsubgd	|- ( ( ph /\ x e. ( SubGrp ` G ) ) -> x = B )
9		velsn	|- ( x e. { B } <-> x = B )
10	8 9	sylibr	|- ( ( ph /\ x e. ( SubGrp ` G ) ) -> x e. { B } )
11	10	ex	|- ( ph -> ( x e. ( SubGrp ` G ) -> x e. { B } ) )
12	11	ssrdv	|- ( ph -> ( SubGrp ` G ) C_ { B } )
13	1	subgid	|- ( G e. Grp -> B e. ( SubGrp ` G ) )
14	3 13	syl	|- ( ph -> B e. ( SubGrp ` G ) )
15	14	snssd	|- ( ph -> { B } C_ ( SubGrp ` G ) )
16	12 15	eqssd	|- ( ph -> ( SubGrp ` G ) = { B } )