Definition df-rngim

Description: Define the set of non-unital ring isomorphisms from r to s . (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Assertion	df-rngim	|- RngIso = ( r e. _V , s e. _V |-> { f e. ( r RngHom s ) | `' f e. ( s RngHom r ) } )

Detailed syntax breakdown

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