Detailed syntax breakdown of Definition df-zrng
Step | Hyp | Ref
| Expression |
1 | | czr 32897 |
. 2
class
ZRing |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | cvv 3486 |
. . 3
class
V |
4 | 2 | cv 1536 |
. . . 4
class 𝑟 |
5 | | czrh 20630 |
. . . . . 6
class
ℤRHom |
6 | 4, 5 | cfv 6341 |
. . . . 5
class
(ℤRHom‘𝑟) |
7 | 6 | crn 5542 |
. . . 4
class ran
(ℤRHom‘𝑟) |
8 | | citr 32881 |
. . . 4
class
IntgRing |
9 | 4, 7, 8 | co 7142 |
. . 3
class (𝑟 IntgRing ran
(ℤRHom‘𝑟)) |
10 | 2, 3, 9 | cmpt 5132 |
. 2
class (𝑟 ∈ V ↦ (𝑟 IntgRing ran
(ℤRHom‘𝑟))) |
11 | 1, 10 | wceq 1537 |
1
wff ZRing =
(𝑟 ∈ V ↦ (𝑟 IntgRing ran
(ℤRHom‘𝑟))) |