MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rngiso Unicode version

Definition df-rngiso 15513
Description: Define the set of ring isomorphisms from  r to  s. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Assertion
Ref Expression
df-rngiso  |- RingIso  =  ( r  e.  _V , 
s  e.  _V  |->  { f  e.  ( r RingHom 
s )  |  `' f  e.  ( s RingHom  r ) } )
Distinct variable group:    s, r, f

Detailed syntax breakdown of Definition df-rngiso
StepHypRef Expression
1 crs 15511 . 2  class RingIso
2 vr . . 3  set  r
3 vs . . 3  set  s
4 cvv 2801 . . 3  class  _V
5 vf . . . . . . 7  set  f
65cv 1631 . . . . . 6  class  f
76ccnv 4704 . . . . 5  class  `' f
83cv 1631 . . . . . 6  class  s
92cv 1631 . . . . . 6  class  r
10 crh 15510 . . . . . 6  class RingHom
118, 9, 10co 5874 . . . . 5  class  ( s RingHom 
r )
127, 11wcel 1696 . . . 4  wff  `' f  e.  ( s RingHom  r
)
139, 8, 10co 5874 . . . 4  class  ( r RingHom 
s )
1412, 5, 13crab 2560 . . 3  class  { f  e.  ( r RingHom  s
)  |  `' f  e.  ( s RingHom  r
) }
152, 3, 4, 4, 14cmpt2 5876 . 2  class  ( r  e.  _V ,  s  e.  _V  |->  { f  e.  ( r RingHom  s
)  |  `' f  e.  ( s RingHom  r
) } )
161, 15wceq 1632 1  wff RingIso  =  ( r  e.  _V , 
s  e.  _V  |->  { f  e.  ( r RingHom 
s )  |  `' f  e.  ( s RingHom  r ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator