Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rngoiso Structured version   Unicode version

Definition df-rngoiso 30619
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
StepHypRef Expression
1 crngiso 30604 . 2  class  RngIso
2 vr . . 3  setvar  r
3 vs . . 3  setvar  s
4 crngo 25575 . . 3  class  RingOps
52cv 1397 . . . . . . 7  class  r
6 c1st 6771 . . . . . . 7  class  1st
75, 6cfv 5570 . . . . . 6  class  ( 1st `  r )
87crn 4989 . . . . 5  class  ran  ( 1st `  r )
93cv 1397 . . . . . . 7  class  s
109, 6cfv 5570 . . . . . 6  class  ( 1st `  s )
1110crn 4989 . . . . 5  class  ran  ( 1st `  s )
12 vf . . . . . 6  setvar  f
1312cv 1397 . . . . 5  class  f
148, 11, 13wf1o 5569 . . . 4  wff  f : ran  ( 1st `  r
)
-1-1-onto-> ran  ( 1st `  s
)
15 crnghom 30603 . . . . 5  class  RngHom
165, 9, 15co 6270 . . . 4  class  ( r 
RngHom  s )
1714, 12, 16crab 2808 . . 3  class  { f  e.  ( r  RngHom  s )  |  f : ran  ( 1st `  r
)
-1-1-onto-> ran  ( 1st `  s
) }
182, 3, 4, 4, 17cmpt2 6272 . 2  class  ( r  e.  RingOps ,  s  e.  RingOps 
|->  { f  e.  ( r  RngHom  s )  |  f : ran  ( 1st `  r ) -1-1-onto-> ran  ( 1st `  s ) } )
191, 18wceq 1398 1  wff  RngIso  =  ( r  e.  RingOps ,  s  e.  RingOps  |->  { f  e.  ( r  RngHom  s )  |  f : ran  ( 1st `  r ) -1-1-onto-> ran  ( 1st `  s
) } )
Colors of variables: wff setvar class
This definition is referenced by:  rngoisoval  30620
  Copyright terms: Public domain W3C validator