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