Definition df-rngoiso 33775

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

Assertion

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

Distinct variable group:   s, r, f

Detailed syntax breakdown of Definition df-rngoiso

Step	Hyp	Ref	Expression
1		crngiso 33760	. 2 class RngIso
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		crngo 33693	. . 3 class RingOps
5	2	cv 1482	. . . . . . 7 class r
6		c1st 7166	. . . . . . 7 class 1st
7	5, 6	cfv 5888	. . . . . 6 class ( 1st ` r )
8	7	crn 5115	. . . . 5 class ran ( 1st ` r )
9	3	cv 1482	. . . . . . 7 class s
10	9, 6	cfv 5888	. . . . . 6 class ( 1st ` s )
11	10	crn 5115	. . . . 5 class ran ( 1st ` s )
12		vf	. . . . . 6 setvar f
13	12	cv 1482	. . . . 5 class f
14	8, 11, 13	wf1o 5887	. . . 4 wff f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s )
15		crnghom 33759	. . . . 5 class RngHom
16	5, 9, 15	co 6650	. . . 4 class ( r RngHom s )
17	14, 12, 16	crab 2916	. . 3 class { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) }
18	2, 3, 4, 4, 17	cmpt2 6652	. 2 class ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )
19	1, 18	wceq 1483	1 wff RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } )

This definition is referenced by:  rngoisoval  33776