Detailed syntax breakdown of Definition df-irng
Step | Hyp | Ref
| Expression |
1 | | citr 30776 |
. 2
class
IntgRing |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | vf |
. . . 4
setvar 𝑓 |
6 | 2 | cv 1474 |
. . . . . 6
class 𝑟 |
7 | 3 | cv 1474 |
. . . . . 6
class 𝑠 |
8 | | cress 15696 |
. . . . . 6
class
↾s |
9 | 6, 7, 8 | co 6549 |
. . . . 5
class (𝑟 ↾s 𝑠) |
10 | | cmn1 23689 |
. . . . 5
class
Monic1p |
11 | 9, 10 | cfv 5804 |
. . . 4
class
(Monic1p‘(𝑟 ↾s 𝑠)) |
12 | 5 | cv 1474 |
. . . . . 6
class 𝑓 |
13 | 12 | ccnv 5037 |
. . . . 5
class ◡𝑓 |
14 | | c0g 15923 |
. . . . . . 7
class
0g |
15 | 6, 14 | cfv 5804 |
. . . . . 6
class
(0g‘𝑟) |
16 | 15 | csn 4125 |
. . . . 5
class
{(0g‘𝑟)} |
17 | 13, 16 | cima 5041 |
. . . 4
class (◡𝑓 “ {(0g‘𝑟)}) |
18 | 5, 11, 17 | ciun 4455 |
. . 3
class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}) |
19 | 2, 3, 4, 4, 18 | cmpt2 6551 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})) |
20 | 1, 19 | wceq 1475 |
1
wff IntgRing =
(𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})) |