Detailed syntax breakdown of Definition df-igen
Step | Hyp | Ref
| Expression |
1 | | cigen 36144 |
. 2
class
IdlGen |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | crngo 35979 |
. . 3
class
RingOps |
5 | 2 | cv 1538 |
. . . . . 6
class 𝑟 |
6 | | c1st 7802 |
. . . . . 6
class
1st |
7 | 5, 6 | cfv 6418 |
. . . . 5
class
(1st ‘𝑟) |
8 | 7 | crn 5581 |
. . . 4
class ran
(1st ‘𝑟) |
9 | 8 | cpw 4530 |
. . 3
class 𝒫
ran (1st ‘𝑟) |
10 | 3 | cv 1538 |
. . . . . 6
class 𝑠 |
11 | | vj |
. . . . . . 7
setvar 𝑗 |
12 | 11 | cv 1538 |
. . . . . 6
class 𝑗 |
13 | 10, 12 | wss 3883 |
. . . . 5
wff 𝑠 ⊆ 𝑗 |
14 | | cidl 36092 |
. . . . . 6
class
Idl |
15 | 5, 14 | cfv 6418 |
. . . . 5
class
(Idl‘𝑟) |
16 | 13, 11, 15 | crab 3067 |
. . . 4
class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗} |
17 | 16 | cint 4876 |
. . 3
class ∩ {𝑗
∈ (Idl‘𝑟)
∣ 𝑠 ⊆ 𝑗} |
18 | 2, 3, 4, 9, 17 | cmpo 7257 |
. 2
class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran
(1st ‘𝑟)
↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) |
19 | 1, 18 | wceq 1539 |
1
wff IdlGen =
(𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran
(1st ‘𝑟)
↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) |