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 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
StepHypRef Expression
1 crisc 32931 . 2 class 𝑟
2 vr . . . . . . 7 setvar 𝑟
32cv 1474 . . . . . 6 class 𝑟
4 crngo 32863 . . . . . 6 class RingOps
53, 4wcel 1977 . . . . 5 wff 𝑟 ∈ RingOps
6 vs . . . . . . 7 setvar 𝑠
76cv 1474 . . . . . 6 class 𝑠
87, 4wcel 1977 . . . . 5 wff 𝑠 ∈ RingOps
95, 8wa 383 . . . 4 wff (𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps)
10 vf . . . . . . 7 setvar 𝑓
1110cv 1474 . . . . . 6 class 𝑓
12 crngiso 32930 . . . . . . 7 class RngIso
133, 7, 12co 6549 . . . . . 6 class (𝑟 RngIso 𝑠)
1411, 13wcel 1977 . . . . 5 wff 𝑓 ∈ (𝑟 RngIso 𝑠)
1514, 10wex 1695 . . . 4 wff 𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)
169, 15wa 383 . . 3 wff ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))
1716, 2, 6copab 4642 . 2 class {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}
181, 17wceq 1475 1 wff 𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}
 Colors of variables: wff setvar class This definition is referenced by:  isriscg  32953  riscer  32957
 Copyright terms: Public domain W3C validator