Detailed syntax breakdown of Definition df-lp
Step | Hyp | Ref
| Expression |
1 | | clp 21878 |
. 2
class
limPt |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | ctop 21637 |
. . 3
class
Top |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | 2 | cv 1541 |
. . . . . 6
class 𝑗 |
6 | 5 | cuni 4793 |
. . . . 5
class ∪ 𝑗 |
7 | 6 | cpw 4485 |
. . . 4
class 𝒫
∪ 𝑗 |
8 | | vy |
. . . . . . 7
setvar 𝑦 |
9 | 8 | cv 1541 |
. . . . . 6
class 𝑦 |
10 | 4 | cv 1541 |
. . . . . . . 8
class 𝑥 |
11 | 9 | csn 4513 |
. . . . . . . 8
class {𝑦} |
12 | 10, 11 | cdif 3838 |
. . . . . . 7
class (𝑥 ∖ {𝑦}) |
13 | | ccl 21762 |
. . . . . . . 8
class
cls |
14 | 5, 13 | cfv 6333 |
. . . . . . 7
class
(cls‘𝑗) |
15 | 12, 14 | cfv 6333 |
. . . . . 6
class
((cls‘𝑗)‘(𝑥 ∖ {𝑦})) |
16 | 9, 15 | wcel 2113 |
. . . . 5
wff 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦})) |
17 | 16, 8 | cab 2716 |
. . . 4
class {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))} |
18 | 4, 7, 17 | cmpt 5107 |
. . 3
class (𝑥 ∈ 𝒫 ∪ 𝑗
↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}) |
19 | 2, 3, 18 | cmpt 5107 |
. 2
class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})) |
20 | 1, 19 | wceq 1542 |
1
wff limPt =
(𝑗 ∈ Top ↦
(𝑥 ∈ 𝒫 ∪ 𝑗
↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})) |