Detailed syntax breakdown of Definition df-utop
Step | Hyp | Ref
| Expression |
1 | | cutop 23380 |
. 2
class
unifTop |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | cust 23349 |
. . . . 5
class
UnifOn |
4 | 3 | crn 5592 |
. . . 4
class ran
UnifOn |
5 | 4 | cuni 4841 |
. . 3
class ∪ ran UnifOn |
6 | | vv |
. . . . . . . . 9
setvar 𝑣 |
7 | 6 | cv 1538 |
. . . . . . . 8
class 𝑣 |
8 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
9 | 8 | cv 1538 |
. . . . . . . . 9
class 𝑥 |
10 | 9 | csn 4563 |
. . . . . . . 8
class {𝑥} |
11 | 7, 10 | cima 5594 |
. . . . . . 7
class (𝑣 “ {𝑥}) |
12 | | va |
. . . . . . . 8
setvar 𝑎 |
13 | 12 | cv 1538 |
. . . . . . 7
class 𝑎 |
14 | 11, 13 | wss 3888 |
. . . . . 6
wff (𝑣 “ {𝑥}) ⊆ 𝑎 |
15 | 2 | cv 1538 |
. . . . . 6
class 𝑢 |
16 | 14, 6, 15 | wrex 3065 |
. . . . 5
wff
∃𝑣 ∈
𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎 |
17 | 16, 8, 13 | wral 3064 |
. . . 4
wff
∀𝑥 ∈
𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎 |
18 | 15 | cuni 4841 |
. . . . . 6
class ∪ 𝑢 |
19 | 18 | cdm 5591 |
. . . . 5
class dom ∪ 𝑢 |
20 | 19 | cpw 4535 |
. . . 4
class 𝒫
dom ∪ 𝑢 |
21 | 17, 12, 20 | crab 3068 |
. . 3
class {𝑎 ∈ 𝒫 dom ∪ 𝑢
∣ ∀𝑥 ∈
𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎} |
22 | 2, 5, 21 | cmpt 5159 |
. 2
class (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢
∣ ∀𝑥 ∈
𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}) |
23 | 1, 22 | wceq 1539 |
1
wff unifTop =
(𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢
∣ ∀𝑥 ∈
𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}) |