Step |
Hyp |
Ref |
Expression |
1 |
|
gicen.b |
|- B = ( Base ` R ) |
2 |
|
gicen.c |
|- C = ( Base ` S ) |
3 |
|
brgic |
|- ( R ~=g S <-> ( R GrpIso S ) =/= (/) ) |
4 |
|
n0 |
|- ( ( R GrpIso S ) =/= (/) <-> E. f f e. ( R GrpIso S ) ) |
5 |
1 2
|
gimf1o |
|- ( f e. ( R GrpIso S ) -> f : B -1-1-onto-> C ) |
6 |
1
|
fvexi |
|- B e. _V |
7 |
6
|
f1oen |
|- ( f : B -1-1-onto-> C -> B ~~ C ) |
8 |
5 7
|
syl |
|- ( f e. ( R GrpIso S ) -> B ~~ C ) |
9 |
8
|
exlimiv |
|- ( E. f f e. ( R GrpIso S ) -> B ~~ C ) |
10 |
4 9
|
sylbi |
|- ( ( R GrpIso S ) =/= (/) -> B ~~ C ) |
11 |
3 10
|
sylbi |
|- ( R ~=g S -> B ~~ C ) |