Detailed syntax breakdown of Definition df-igen
Step | Hyp | Ref
| Expression |
1 | | cigen 35840 |
. 2
class
IdlGen |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | crngo 35675 |
. . 3
class
RingOps |
5 | 2 | cv 1541 |
. . . . . 6
class 𝑟 |
6 | | c1st 7712 |
. . . . . 6
class
1st |
7 | 5, 6 | cfv 6339 |
. . . . 5
class
(1st ‘𝑟) |
8 | 7 | crn 5526 |
. . . 4
class ran
(1st ‘𝑟) |
9 | 8 | cpw 4488 |
. . 3
class 𝒫
ran (1st ‘𝑟) |
10 | 3 | cv 1541 |
. . . . . 6
class 𝑠 |
11 | | vj |
. . . . . . 7
setvar 𝑗 |
12 | 11 | cv 1541 |
. . . . . 6
class 𝑗 |
13 | 10, 12 | wss 3843 |
. . . . 5
wff 𝑠 ⊆ 𝑗 |
14 | | cidl 35788 |
. . . . . 6
class
Idl |
15 | 5, 14 | cfv 6339 |
. . . . 5
class
(Idl‘𝑟) |
16 | 13, 11, 15 | crab 3057 |
. . . 4
class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗} |
17 | 16 | cint 4836 |
. . 3
class ∩ {𝑗
∈ (Idl‘𝑟)
∣ 𝑠 ⊆ 𝑗} |
18 | 2, 3, 4, 9, 17 | cmpo 7172 |
. 2
class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran
(1st ‘𝑟)
↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) |
19 | 1, 18 | wceq 1542 |
1
wff IdlGen =
(𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran
(1st ‘𝑟)
↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) |