Theorem rngoisoval

Description: The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngisoval.1	|- G = ( 1st ` R )
	rngisoval.2	|- X = ran G
	rngisoval.3	|- J = ( 1st ` S )
	rngisoval.4	|- Y = ran J
Assertion	rngoisoval	|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngIso S ) = { f e. ( R RngHom S ) | f : X -1-1-onto-> Y } )

Proof

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 RngHom s ) = ( R RngHom 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 RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } = { f e. ( R RngHom S ) | f : X -1-1-onto-> Y } )
18		df-rngoiso	|- RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )
19		ovex	|- ( R RngHom S ) e. _V
20	19	rabex	|- { f e. ( R RngHom S ) | f : X -1-1-onto-> Y } e. _V
21	17 18 20	ovmpoa	|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngIso S ) = { f e. ( R RngHom S ) | f : X -1-1-onto-> Y } )