Definition df-rngoiso

Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Assertion	df-rngoiso	|- RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crngiso	|- RngIso
1		vr	|- r
2		crngo	|- RingOps
3		vs	|- s
4		vf	|- f
5	1	cv	|- r
6		crnghom	|- RngHom
7	3	cv	|- s
8	5 7 6	co	|- ( r RngHom s )
9	4	cv	|- f
10		c1st	|- 1st
11	5 10	cfv	|- ( 1st ` r )
12	11	crn	|- ran ( 1st ` r )
13	7 10	cfv	|- ( 1st ` s )
14	13	crn	|- ran ( 1st ` s )
15	12 14 9	wf1o	|- f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s )
16	15 4 8	crab	|- { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) }
17	1 3 2 2 16	cmpo	|- ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )
18	0 17	wceq	|- RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )