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