This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 = 𝐵 )