Detailed syntax breakdown of Definition df-irng
Step | Hyp | Ref
| Expression |
1 | | citr 31522 |
. 2
class
IntgRing |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3200 |
. . 3
class
V |
5 | | vf |
. . . 4
setvar 𝑓 |
6 | 2 | cv 1482 |
. . . . . 6
class 𝑟 |
7 | 3 | cv 1482 |
. . . . . 6
class 𝑠 |
8 | | cress 15858 |
. . . . . 6
class
↾s |
9 | 6, 7, 8 | co 6650 |
. . . . 5
class (𝑟 ↾s 𝑠) |
10 | | cmn1 23885 |
. . . . 5
class
Monic1p |
11 | 9, 10 | cfv 5888 |
. . . 4
class
(Monic1p‘(𝑟 ↾s 𝑠)) |
12 | 5 | cv 1482 |
. . . . . 6
class 𝑓 |
13 | 12 | ccnv 5113 |
. . . . 5
class ◡𝑓 |
14 | | c0g 16100 |
. . . . . . 7
class
0g |
15 | 6, 14 | cfv 5888 |
. . . . . 6
class
(0g‘𝑟) |
16 | 15 | csn 4177 |
. . . . 5
class
{(0g‘𝑟)} |
17 | 13, 16 | cima 5117 |
. . . 4
class (◡𝑓 “ {(0g‘𝑟)}) |
18 | 5, 11, 17 | ciun 4520 |
. . 3
class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}) |
19 | 2, 3, 4, 4, 18 | cmpt2 6652 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})) |
20 | 1, 19 | wceq 1483 |
1
wff IntgRing =
(𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})) |