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

Definition df-rngoiso 26607
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 26592 . 2  class  RngIso
2 vr . . 3  set  r
3 vs . . 3  set  s
4 crngo 21042 . . 3  class  RingOps
52cv 1622 . . . . . . 7  class  r
6 c1st 6120 . . . . . . 7  class  1st
75, 6cfv 5255 . . . . . 6  class  ( 1st `  r )
87crn 4690 . . . . 5  class  ran  ( 1st `  r )
93cv 1622 . . . . . . 7  class  s
109, 6cfv 5255 . . . . . 6  class  ( 1st `  s )
1110crn 4690 . . . . 5  class  ran  ( 1st `  s )
12 vf . . . . . 6  set  f
1312cv 1622 . . . . 5  class  f
148, 11, 13wf1o 5254 . . . 4  wff  f : ran  ( 1st `  r
)
-1-1-onto-> ran  ( 1st `  s
)
15 crnghom 26591 . . . . 5  class  RngHom
165, 9, 15co 5858 . . . 4  class  ( r 
RngHom  s )
1714, 12, 16crab 2547 . . 3  class  { f  e.  ( r  RngHom  s )  |  f : ran  ( 1st `  r
)
-1-1-onto-> ran  ( 1st `  s
) }
182, 3, 4, 4, 17cmpt2 5860 . 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 1623 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 set class
This definition is referenced by:  rngoisoval  26608
  Copyright terms: Public domain W3C validator