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

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

Metamath Proof Explorer