Definition df-risc 32952

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

Assertion

Ref	Expression
df-risc	⊢ ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}

Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-risc

Step	Hyp	Ref	Expression
1		crisc 32931	. 2 class ≃𝑟
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1474	. . . . . 6 class 𝑟
4		crngo 32863	. . . . . 6 class RingOps
5	3, 4	wcel 1977	. . . . 5 wff 𝑟 ∈ RingOps
6		vs	. . . . . . 7 setvar 𝑠
7	6	cv 1474	. . . . . 6 class 𝑠
8	7, 4	wcel 1977	. . . . 5 wff 𝑠 ∈ RingOps
9	5, 8	wa 383	. . . 4 wff (𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps)
10		vf	. . . . . . 7 setvar 𝑓
11	10	cv 1474	. . . . . 6 class 𝑓
12		crngiso 32930	. . . . . . 7 class RngIso
13	3, 7, 12	co 6549	. . . . . 6 class (𝑟 RngIso 𝑠)
14	11, 13	wcel 1977	. . . . 5 wff 𝑓 ∈ (𝑟 RngIso 𝑠)
15	14, 10	wex 1695	. . . 4 wff ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)
16	9, 15	wa 383	. . 3 wff ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))
17	16, 2, 6	copab 4642	. 2 class {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}
18	1, 17	wceq 1475	1 wff ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}

This definition is referenced by:  isriscg  32953  riscer  32957