Metamath Proof Explorer
Description: Define a function on topologies whose value is the set of closed sets of
the topology. (Contributed by NM, 2-Oct-2006)
|
|
Ref |
Expression |
|
Assertion |
df-cld |
⊢ Clsd = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } ) |
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
ccld |
⊢ Clsd |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vx |
⊢ 𝑥 |
4 |
1
|
cv |
⊢ 𝑗 |
5 |
4
|
cuni |
⊢ ∪ 𝑗 |
6 |
5
|
cpw |
⊢ 𝒫 ∪ 𝑗 |
7 |
3
|
cv |
⊢ 𝑥 |
8 |
5 7
|
cdif |
⊢ ( ∪ 𝑗 ∖ 𝑥 ) |
9 |
8 4
|
wcel |
⊢ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 |
10 |
9 3 6
|
crab |
⊢ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } |
11 |
1 2 10
|
cmpt |
⊢ ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } ) |
12 |
0 11
|
wceq |
⊢ Clsd = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } ) |