Step |
Hyp |
Ref |
Expression |
1 |
|
subgim.b |
|- B = ( Base ` R ) |
2 |
|
gimghm |
|- ( F e. ( R GrpIso S ) -> F e. ( R GrpHom S ) ) |
3 |
2
|
adantr |
|- ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> F e. ( R GrpHom S ) ) |
4 |
|
ghmima |
|- ( ( F e. ( R GrpHom S ) /\ A e. ( SubGrp ` R ) ) -> ( F " A ) e. ( SubGrp ` S ) ) |
5 |
3 4
|
sylan |
|- ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ A e. ( SubGrp ` R ) ) -> ( F " A ) e. ( SubGrp ` S ) ) |
6 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
7 |
1 6
|
gimf1o |
|- ( F e. ( R GrpIso S ) -> F : B -1-1-onto-> ( Base ` S ) ) |
8 |
|
f1of1 |
|- ( F : B -1-1-onto-> ( Base ` S ) -> F : B -1-1-> ( Base ` S ) ) |
9 |
7 8
|
syl |
|- ( F e. ( R GrpIso S ) -> F : B -1-1-> ( Base ` S ) ) |
10 |
|
f1imacnv |
|- ( ( F : B -1-1-> ( Base ` S ) /\ A C_ B ) -> ( `' F " ( F " A ) ) = A ) |
11 |
9 10
|
sylan |
|- ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> ( `' F " ( F " A ) ) = A ) |
12 |
11
|
adantr |
|- ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> ( `' F " ( F " A ) ) = A ) |
13 |
|
ghmpreima |
|- ( ( F e. ( R GrpHom S ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> ( `' F " ( F " A ) ) e. ( SubGrp ` R ) ) |
14 |
3 13
|
sylan |
|- ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> ( `' F " ( F " A ) ) e. ( SubGrp ` R ) ) |
15 |
12 14
|
eqeltrrd |
|- ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> A e. ( SubGrp ` R ) ) |
16 |
5 15
|
impbida |
|- ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> ( A e. ( SubGrp ` R ) <-> ( F " A ) e. ( SubGrp ` S ) ) ) |