Detailed syntax breakdown of Definition df-rspec
Step | Hyp | Ref
| Expression |
1 | | crspec 31526 |
. 2
class
Spec |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | crg 19562 |
. . 3
class
Ring |
4 | 2 | cv 1542 |
. . . . 5
class 𝑟 |
5 | | cidlsrg 31359 |
. . . . 5
class
IDLsrg |
6 | 4, 5 | cfv 6380 |
. . . 4
class
(IDLsrg‘𝑟) |
7 | | cprmidl 31324 |
. . . . 5
class
PrmIdeal |
8 | 4, 7 | cfv 6380 |
. . . 4
class
(PrmIdeal‘𝑟) |
9 | | cress 16784 |
. . . 4
class
↾s |
10 | 6, 8, 9 | co 7213 |
. . 3
class
((IDLsrg‘𝑟)
↾s (PrmIdeal‘𝑟)) |
11 | 2, 3, 10 | cmpt 5135 |
. 2
class (𝑟 ∈ Ring ↦
((IDLsrg‘𝑟)
↾s (PrmIdeal‘𝑟))) |
12 | 1, 11 | wceq 1543 |
1
wff Spec =
(𝑟 ∈ Ring ↦
((IDLsrg‘𝑟)
↾s (PrmIdeal‘𝑟))) |