Definition df-risc 37990

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

Assertion

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

Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-risc

Step	Hyp	Ref	Expression
1		crisc 37969	. 2 class ≃𝑟
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1539	. . . . . 6 class 𝑟
4		crngo 37901	. . . . . 6 class RingOps
5	3, 4	wcel 2108	. . . . 5 wff 𝑟 ∈ RingOps
6		vs	. . . . . . 7 setvar 𝑠
7	6	cv 1539	. . . . . 6 class 𝑠
8	7, 4	wcel 2108	. . . . 5 wff 𝑠 ∈ RingOps
9	5, 8	wa 395	. . . 4 wff (𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps)
10		vf	. . . . . . 7 setvar 𝑓
11	10	cv 1539	. . . . . 6 class 𝑓
12		crngoiso 37968	. . . . . . 7 class RingOpsIso
13	3, 7, 12	co 7431	. . . . . 6 class (𝑟 RingOpsIso 𝑠)
14	11, 13	wcel 2108	. . . . 5 wff 𝑓 ∈ (𝑟 RingOpsIso 𝑠)
15	14, 10	wex 1779	. . . 4 wff ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠)
16	9, 15	wa 395	. . 3 wff ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))
17	16, 2, 6	copab 5205	. 2 class {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))}
18	1, 17	wceq 1540	1 wff ≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))}

This definition is referenced by:  isriscg  37991  riscer  37995