Step |
Hyp |
Ref |
Expression |
0 |
|
cutop |
⊢ unifTop |
1 |
|
vu |
⊢ 𝑢 |
2 |
|
cust |
⊢ UnifOn |
3 |
2
|
crn |
⊢ ran UnifOn |
4 |
3
|
cuni |
⊢ ∪ ran UnifOn |
5 |
|
va |
⊢ 𝑎 |
6 |
1
|
cv |
⊢ 𝑢 |
7 |
6
|
cuni |
⊢ ∪ 𝑢 |
8 |
7
|
cdm |
⊢ dom ∪ 𝑢 |
9 |
8
|
cpw |
⊢ 𝒫 dom ∪ 𝑢 |
10 |
|
vx |
⊢ 𝑥 |
11 |
5
|
cv |
⊢ 𝑎 |
12 |
|
vv |
⊢ 𝑣 |
13 |
12
|
cv |
⊢ 𝑣 |
14 |
10
|
cv |
⊢ 𝑥 |
15 |
14
|
csn |
⊢ { 𝑥 } |
16 |
13 15
|
cima |
⊢ ( 𝑣 “ { 𝑥 } ) |
17 |
16 11
|
wss |
⊢ ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 |
18 |
17 12 6
|
wrex |
⊢ ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 |
19 |
18 10 11
|
wral |
⊢ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 |
20 |
19 5 9
|
crab |
⊢ { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } |
21 |
1 4 20
|
cmpt |
⊢ ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ) |
22 |
0 21
|
wceq |
⊢ unifTop = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ) |