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