Theorem trivsubgsnd

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

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

Proof

Step	Hyp	Ref	Expression
1		trivsubgsnd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		trivsubgsnd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		trivsubgsnd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		trivsubgsnd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Grp )
6	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐵 = { 0 } )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
8	1 2 5 6 7	trivsubgd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑥 = 𝐵 )
9		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
10	8 9	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑥 ∈ { 𝐵 } )
11	10	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ∈ { 𝐵 } ) )
12	11	ssrdv	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ⊆ { 𝐵 } )
13	1	subgid	⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
14	3 13	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
15	14	snssd	⊢ ( 𝜑 → { 𝐵 } ⊆ ( SubGrp ‘ 𝐺 ) )
16	12 15	eqssd	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) = { 𝐵 } )