Detailed syntax breakdown of Definition df-ntr
Step | Hyp | Ref
| Expression |
1 | | cnt 12852 |
. 2
class
int |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | ctop 12754 |
. . 3
class
Top |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | 2 | cv 1347 |
. . . . . 6
class 𝑗 |
6 | 5 | cuni 3794 |
. . . . 5
class ∪ 𝑗 |
7 | 6 | cpw 3564 |
. . . 4
class 𝒫
∪ 𝑗 |
8 | 4 | cv 1347 |
. . . . . . 7
class 𝑥 |
9 | 8 | cpw 3564 |
. . . . . 6
class 𝒫
𝑥 |
10 | 5, 9 | cin 3120 |
. . . . 5
class (𝑗 ∩ 𝒫 𝑥) |
11 | 10 | cuni 3794 |
. . . 4
class ∪ (𝑗
∩ 𝒫 𝑥) |
12 | 4, 7, 11 | cmpt 4048 |
. . 3
class (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥)) |
13 | 2, 3, 12 | cmpt 4048 |
. 2
class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) |
14 | 1, 13 | wceq 1348 |
1
wff int =
(𝑗 ∈ Top ↦
(𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) |