Definition df-rim

Description: Define the set of ring isomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	df-rim	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crs	|- RingIso
1		vr	|- r
2		cvv	|- _V
3		vs	|- s
4		vf	|- f
5	1	cv	|- r
6		crh	|- RingHom
7	3	cv	|- s
8	5 7 6	co	|- ( r RingHom s )
9	4	cv	|- f
10	9	ccnv	|- `' f
11	7 5 6	co	|- ( s RingHom r )
12	10 11	wcel	|- `' f e. ( s RingHom r )
13	12 4 8	crab	|- { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) }
14	1 3 2 2 13	cmpo	|- ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
15	0 14	wceq	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )