Detailed syntax breakdown of Definition df-risc
Step | Hyp | Ref
| Expression |
1 | | crisc 36128 |
. 2
class
≃𝑟 |
2 | | vr |
. . . . . . 7
setvar 𝑟 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑟 |
4 | | crngo 36060 |
. . . . . 6
class
RingOps |
5 | 3, 4 | wcel 2106 |
. . . . 5
wff 𝑟 ∈ RingOps |
6 | | vs |
. . . . . . 7
setvar 𝑠 |
7 | 6 | cv 1538 |
. . . . . 6
class 𝑠 |
8 | 7, 4 | wcel 2106 |
. . . . 5
wff 𝑠 ∈ RingOps |
9 | 5, 8 | wa 396 |
. . . 4
wff (𝑟 ∈ RingOps ∧ 𝑠 ∈
RingOps) |
10 | | vf |
. . . . . . 7
setvar 𝑓 |
11 | 10 | cv 1538 |
. . . . . 6
class 𝑓 |
12 | | crngiso 36127 |
. . . . . . 7
class
RngIso |
13 | 3, 7, 12 | co 7267 |
. . . . . 6
class (𝑟 RngIso 𝑠) |
14 | 11, 13 | wcel 2106 |
. . . . 5
wff 𝑓 ∈ (𝑟 RngIso 𝑠) |
15 | 14, 10 | wex 1782 |
. . . 4
wff
∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) |
16 | 9, 15 | wa 396 |
. . 3
wff ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧
∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)) |
17 | 16, 2, 6 | copab 5135 |
. 2
class
{〈𝑟, 𝑠〉 ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧
∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))} |
18 | 1, 17 | wceq 1539 |
1
wff
≃𝑟 = {〈𝑟, 𝑠〉 ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))} |