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 \in V, s \in V ⟼ \{f \in (r RngHomo s) \| f^{-1} \in (s RngHomo r)\})$

Step	Hyp	Ref	Expression
0		crngs	$class RngIsom$
1		vr	$setvar r$
2		cvv	$class V$
3		vs	$setvar s$
4		vf	$setvar f$
5	1	cv	$setvar r$
6		crngh	$class RngHomo$
7	3	cv	$setvar s$
8	5 7 6	co	$class (r RngHomo s)$
9	4	cv	$setvar f$
10	9	ccnv	$class f^{-1}$
11	7 5 6	co	$class (s RngHomo r)$
12	10 11	wcel	$wff f^{-1} \in (s RngHomo r)$
13	12 4 8	crab	$class \{f \in (r RngHomo s) \| f^{-1} \in (s RngHomo r)\}$
14	1 3 2 2 13	cmpo	$class (r \in V, s \in V ⟼ \{f \in (r RngHomo s) \| f^{-1} \in (s RngHomo r)\})$
15	0 14	wceq	$wff RngIsom = (r \in V, s \in V ⟼ \{f \in (r RngHomo s) \| f^{-1} \in (s RngHomo r)\})$

Metamath Proof Explorer