This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cld

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 ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ( ∪ 𝑗 ∖ 𝑥 ) ∈ 𝑗 } )