Definition df-rngisom

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

	Ref	Expression
Assertion	df-rngisom	|- RngIsom = ( r e. _V , s e. _V |-> { f e. ( r RngHomo s ) | `' f e. ( s RngHomo r ) } )

Detailed syntax breakdown

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