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