Metamath Proof Explorer


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 ) } )