Step | Hyp | Ref
| Expression |
1 | | crisc 36424 |
. 2
class
≃𝑟 |
2 | | vr |
. . . . . . 7
setvar 𝑟 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑟 |
4 | | crngo 36356 |
. . . . . 6
class
RingOps |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff 𝑟 ∈ RingOps |
6 | | vs |
. . . . . . 7
setvar 𝑠 |
7 | 6 | cv 1541 |
. . . . . 6
class 𝑠 |
8 | 7, 4 | wcel 2107 |
. . . . 5
wff 𝑠 ∈ RingOps |
9 | 5, 8 | wa 397 |
. . . 4
wff (𝑟 ∈ RingOps ∧ 𝑠 ∈
RingOps) |
10 | | vf |
. . . . . . 7
setvar 𝑓 |
11 | 10 | cv 1541 |
. . . . . 6
class 𝑓 |
12 | | crngiso 36423 |
. . . . . . 7
class
RngIso |
13 | 3, 7, 12 | co 7358 |
. . . . . 6
class (𝑟 RngIso 𝑠) |
14 | 11, 13 | wcel 2107 |
. . . . 5
wff 𝑓 ∈ (𝑟 RngIso 𝑠) |
15 | 14, 10 | wex 1782 |
. . . 4
wff
∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) |
16 | 9, 15 | wa 397 |
. . 3
wff ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧
∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)) |
17 | 16, 2, 6 | copab 5168 |
. 2
class
{⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧
∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))} |
18 | 1, 17 | wceq 1542 |
1
wff
≃𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))} |