Metamath Proof Explorer


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 } )