df-risc

Description: Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

		Ref	Expression
	Assertion	df-risc	$⊢ ≃_{𝑟} = \{⟨r, s⟩ \| ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s))\}$

Step	Hyp	Ref	Expression
0		crisc	$class ≃_{𝑟}$
1		vr	$setvar r$
2		vs	$setvar s$
3	1	cv	$setvar r$
4		crngo	$class RingOps$
5	3 4	wcel	$wff r \in RingOps$
6	2	cv	$setvar s$
7	6 4	wcel	$wff s \in RingOps$
8	5 7	wa	$wff (r \in RingOps \land s \in RingOps)$
9		vf	$setvar f$
10	9	cv	$setvar f$
11		crngiso	$class RngIso$
12	3 6 11	co	$class (r RngIso s)$
13	10 12	wcel	$wff f \in (r RngIso s)$
14	13 9	wex	$wff \exists f f \in (r RngIso s)$
15	8 14	wa	$wff ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s))$
16	15 1 2	copab	$class \{⟨r, s⟩ \| ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s))\}$
17	0 16	wceq	$wff ≃_{𝑟} = \{⟨r, s⟩ \| ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s))\}$

Metamath Proof Explorer