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

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