Step |
Hyp |
Ref |
Expression |
1 |
|
brgic |
|- ( R ~=g S <-> ( R GrpIso S ) =/= (/) ) |
2 |
|
n0 |
|- ( ( R GrpIso S ) =/= (/) <-> E. a a e. ( R GrpIso S ) ) |
3 |
1 2
|
bitri |
|- ( R ~=g S <-> E. a a e. ( R GrpIso S ) ) |
4 |
|
fvexd |
|- ( a e. ( R GrpIso S ) -> ( SubGrp ` R ) e. _V ) |
5 |
|
fvexd |
|- ( a e. ( R GrpIso S ) -> ( SubGrp ` S ) e. _V ) |
6 |
|
vex |
|- a e. _V |
7 |
6
|
imaex |
|- ( a " b ) e. _V |
8 |
7
|
2a1i |
|- ( a e. ( R GrpIso S ) -> ( b e. ( SubGrp ` R ) -> ( a " b ) e. _V ) ) |
9 |
6
|
cnvex |
|- `' a e. _V |
10 |
9
|
imaex |
|- ( `' a " c ) e. _V |
11 |
10
|
2a1i |
|- ( a e. ( R GrpIso S ) -> ( c e. ( SubGrp ` S ) -> ( `' a " c ) e. _V ) ) |
12 |
|
gimghm |
|- ( a e. ( R GrpIso S ) -> a e. ( R GrpHom S ) ) |
13 |
|
ghmima |
|- ( ( a e. ( R GrpHom S ) /\ b e. ( SubGrp ` R ) ) -> ( a " b ) e. ( SubGrp ` S ) ) |
14 |
12 13
|
sylan |
|- ( ( a e. ( R GrpIso S ) /\ b e. ( SubGrp ` R ) ) -> ( a " b ) e. ( SubGrp ` S ) ) |
15 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
16 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
17 |
15 16
|
gimf1o |
|- ( a e. ( R GrpIso S ) -> a : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) |
18 |
|
f1of1 |
|- ( a : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> a : ( Base ` R ) -1-1-> ( Base ` S ) ) |
19 |
17 18
|
syl |
|- ( a e. ( R GrpIso S ) -> a : ( Base ` R ) -1-1-> ( Base ` S ) ) |
20 |
15
|
subgss |
|- ( b e. ( SubGrp ` R ) -> b C_ ( Base ` R ) ) |
21 |
|
f1imacnv |
|- ( ( a : ( Base ` R ) -1-1-> ( Base ` S ) /\ b C_ ( Base ` R ) ) -> ( `' a " ( a " b ) ) = b ) |
22 |
19 20 21
|
syl2an |
|- ( ( a e. ( R GrpIso S ) /\ b e. ( SubGrp ` R ) ) -> ( `' a " ( a " b ) ) = b ) |
23 |
22
|
eqcomd |
|- ( ( a e. ( R GrpIso S ) /\ b e. ( SubGrp ` R ) ) -> b = ( `' a " ( a " b ) ) ) |
24 |
14 23
|
jca |
|- ( ( a e. ( R GrpIso S ) /\ b e. ( SubGrp ` R ) ) -> ( ( a " b ) e. ( SubGrp ` S ) /\ b = ( `' a " ( a " b ) ) ) ) |
25 |
|
eleq1 |
|- ( c = ( a " b ) -> ( c e. ( SubGrp ` S ) <-> ( a " b ) e. ( SubGrp ` S ) ) ) |
26 |
|
imaeq2 |
|- ( c = ( a " b ) -> ( `' a " c ) = ( `' a " ( a " b ) ) ) |
27 |
26
|
eqeq2d |
|- ( c = ( a " b ) -> ( b = ( `' a " c ) <-> b = ( `' a " ( a " b ) ) ) ) |
28 |
25 27
|
anbi12d |
|- ( c = ( a " b ) -> ( ( c e. ( SubGrp ` S ) /\ b = ( `' a " c ) ) <-> ( ( a " b ) e. ( SubGrp ` S ) /\ b = ( `' a " ( a " b ) ) ) ) ) |
29 |
24 28
|
syl5ibrcom |
|- ( ( a e. ( R GrpIso S ) /\ b e. ( SubGrp ` R ) ) -> ( c = ( a " b ) -> ( c e. ( SubGrp ` S ) /\ b = ( `' a " c ) ) ) ) |
30 |
29
|
impr |
|- ( ( a e. ( R GrpIso S ) /\ ( b e. ( SubGrp ` R ) /\ c = ( a " b ) ) ) -> ( c e. ( SubGrp ` S ) /\ b = ( `' a " c ) ) ) |
31 |
|
ghmpreima |
|- ( ( a e. ( R GrpHom S ) /\ c e. ( SubGrp ` S ) ) -> ( `' a " c ) e. ( SubGrp ` R ) ) |
32 |
12 31
|
sylan |
|- ( ( a e. ( R GrpIso S ) /\ c e. ( SubGrp ` S ) ) -> ( `' a " c ) e. ( SubGrp ` R ) ) |
33 |
|
f1ofo |
|- ( a : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> a : ( Base ` R ) -onto-> ( Base ` S ) ) |
34 |
17 33
|
syl |
|- ( a e. ( R GrpIso S ) -> a : ( Base ` R ) -onto-> ( Base ` S ) ) |
35 |
16
|
subgss |
|- ( c e. ( SubGrp ` S ) -> c C_ ( Base ` S ) ) |
36 |
|
foimacnv |
|- ( ( a : ( Base ` R ) -onto-> ( Base ` S ) /\ c C_ ( Base ` S ) ) -> ( a " ( `' a " c ) ) = c ) |
37 |
34 35 36
|
syl2an |
|- ( ( a e. ( R GrpIso S ) /\ c e. ( SubGrp ` S ) ) -> ( a " ( `' a " c ) ) = c ) |
38 |
37
|
eqcomd |
|- ( ( a e. ( R GrpIso S ) /\ c e. ( SubGrp ` S ) ) -> c = ( a " ( `' a " c ) ) ) |
39 |
32 38
|
jca |
|- ( ( a e. ( R GrpIso S ) /\ c e. ( SubGrp ` S ) ) -> ( ( `' a " c ) e. ( SubGrp ` R ) /\ c = ( a " ( `' a " c ) ) ) ) |
40 |
|
eleq1 |
|- ( b = ( `' a " c ) -> ( b e. ( SubGrp ` R ) <-> ( `' a " c ) e. ( SubGrp ` R ) ) ) |
41 |
|
imaeq2 |
|- ( b = ( `' a " c ) -> ( a " b ) = ( a " ( `' a " c ) ) ) |
42 |
41
|
eqeq2d |
|- ( b = ( `' a " c ) -> ( c = ( a " b ) <-> c = ( a " ( `' a " c ) ) ) ) |
43 |
40 42
|
anbi12d |
|- ( b = ( `' a " c ) -> ( ( b e. ( SubGrp ` R ) /\ c = ( a " b ) ) <-> ( ( `' a " c ) e. ( SubGrp ` R ) /\ c = ( a " ( `' a " c ) ) ) ) ) |
44 |
39 43
|
syl5ibrcom |
|- ( ( a e. ( R GrpIso S ) /\ c e. ( SubGrp ` S ) ) -> ( b = ( `' a " c ) -> ( b e. ( SubGrp ` R ) /\ c = ( a " b ) ) ) ) |
45 |
44
|
impr |
|- ( ( a e. ( R GrpIso S ) /\ ( c e. ( SubGrp ` S ) /\ b = ( `' a " c ) ) ) -> ( b e. ( SubGrp ` R ) /\ c = ( a " b ) ) ) |
46 |
30 45
|
impbida |
|- ( a e. ( R GrpIso S ) -> ( ( b e. ( SubGrp ` R ) /\ c = ( a " b ) ) <-> ( c e. ( SubGrp ` S ) /\ b = ( `' a " c ) ) ) ) |
47 |
4 5 8 11 46
|
en2d |
|- ( a e. ( R GrpIso S ) -> ( SubGrp ` R ) ~~ ( SubGrp ` S ) ) |
48 |
47
|
exlimiv |
|- ( E. a a e. ( R GrpIso S ) -> ( SubGrp ` R ) ~~ ( SubGrp ` S ) ) |
49 |
3 48
|
sylbi |
|- ( R ~=g S -> ( SubGrp ` R ) ~~ ( SubGrp ` S ) ) |