| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rngisoval.1 |
|- G = ( 1st ` R ) |
| 2 |
|
rngisoval.2 |
|- X = ran G |
| 3 |
|
rngisoval.3 |
|- J = ( 1st ` S ) |
| 4 |
|
rngisoval.4 |
|- Y = ran J |
| 5 |
|
oveq12 |
|- ( ( r = R /\ s = S ) -> ( r RingOpsHom s ) = ( R RingOpsHom S ) ) |
| 6 |
|
fveq2 |
|- ( r = R -> ( 1st ` r ) = ( 1st ` R ) ) |
| 7 |
6 1
|
eqtr4di |
|- ( r = R -> ( 1st ` r ) = G ) |
| 8 |
7
|
rneqd |
|- ( r = R -> ran ( 1st ` r ) = ran G ) |
| 9 |
8 2
|
eqtr4di |
|- ( r = R -> ran ( 1st ` r ) = X ) |
| 10 |
9
|
f1oeq2d |
|- ( r = R -> ( f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) <-> f : X -1-1-onto-> ran ( 1st ` s ) ) ) |
| 11 |
|
fveq2 |
|- ( s = S -> ( 1st ` s ) = ( 1st ` S ) ) |
| 12 |
11 3
|
eqtr4di |
|- ( s = S -> ( 1st ` s ) = J ) |
| 13 |
12
|
rneqd |
|- ( s = S -> ran ( 1st ` s ) = ran J ) |
| 14 |
13 4
|
eqtr4di |
|- ( s = S -> ran ( 1st ` s ) = Y ) |
| 15 |
14
|
f1oeq3d |
|- ( s = S -> ( f : X -1-1-onto-> ran ( 1st ` s ) <-> f : X -1-1-onto-> Y ) ) |
| 16 |
10 15
|
sylan9bb |
|- ( ( r = R /\ s = S ) -> ( f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) <-> f : X -1-1-onto-> Y ) ) |
| 17 |
5 16
|
rabeqbidv |
|- ( ( r = R /\ s = S ) -> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) |
| 18 |
|
df-rngoiso |
|- RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) |
| 19 |
|
ovex |
|- ( R RingOpsHom S ) e. _V |
| 20 |
19
|
rabex |
|- { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } e. _V |
| 21 |
17 18 20
|
ovmpoa |
|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) |