Theorem trivsubgd

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

	Ref	Expression
Hypotheses	trivsubgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	trivsubgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	trivsubgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	trivsubgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
	trivsubgd.5	⊢ ( 𝜑 → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
Assertion	trivsubgd	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		trivsubgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		trivsubgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		trivsubgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		trivsubgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
5		trivsubgd.5	⊢ ( 𝜑 → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
6	1	subgss	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 ⊆ 𝐵 )
7	5 6	syl	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
8	7 4	sseqtrd	⊢ ( 𝜑 → 𝐴 ⊆ { 0 } )
9	2	subg0cl	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝐴 )
10	5 9	syl	⊢ ( 𝜑 → 0 ∈ 𝐴 )
11	10	snssd	⊢ ( 𝜑 → { 0 } ⊆ 𝐴 )
12	8 11	eqssd	⊢ ( 𝜑 → 𝐴 = { 0 } )
13	12 4	eqtr4d	⊢ ( 𝜑 → 𝐴 = 𝐵 )