Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-risc Structured version   Visualization version   GIF version

Definition df-risc 35321
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
StepHypRef Expression
1 crisc 35300 . 2 class 𝑟
2 vr . . . . . . 7 setvar 𝑟
32cv 1537 . . . . . 6 class 𝑟
4 crngo 35232 . . . . . 6 class RingOps
53, 4wcel 2115 . . . . 5 wff 𝑟 ∈ RingOps
6 vs . . . . . . 7 setvar 𝑠
76cv 1537 . . . . . 6 class 𝑠
87, 4wcel 2115 . . . . 5 wff 𝑠 ∈ RingOps
95, 8wa 399 . . . 4 wff (𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps)
10 vf . . . . . . 7 setvar 𝑓
1110cv 1537 . . . . . 6 class 𝑓
12 crngiso 35299 . . . . . . 7 class RngIso
133, 7, 12co 7138 . . . . . 6 class (𝑟 RngIso 𝑠)
1411, 13wcel 2115 . . . . 5 wff 𝑓 ∈ (𝑟 RngIso 𝑠)
1514, 10wex 1781 . . . 4 wff 𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)
169, 15wa 399 . . 3 wff ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))
1716, 2, 6copab 5109 . 2 class {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}
181, 17wceq 1538 1 wff 𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}
Colors of variables: wff setvar class
This definition is referenced by:  isriscg  35322  riscer  35326
  Copyright terms: Public domain W3C validator