Definition df-cls

Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval . (Contributed by NM, 3-Oct-2006)

	Ref	Expression
Assertion	df-cls	⊢ cls = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccl	⊢ cls
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6	5	cpw	⊢ 𝒫 ∪ 𝑗
7		vy	⊢ 𝑦
8		ccld	⊢ Clsd
9	4 8	cfv	⊢ ( Clsd ‘ 𝑗 )
10	3	cv	⊢ 𝑥
11	7	cv	⊢ 𝑦
12	10 11	wss	⊢ 𝑥 ⊆ 𝑦
13	12 7 9	crab	⊢ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 }
14	13	cint	⊢ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 }
15	3 6 14	cmpt	⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } )
16	1 2 15	cmpt	⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } ) )
17	0 16	wceq	⊢ cls = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ { 𝑦 ∈ ( Clsd ‘ 𝑗 ) ∣ 𝑥 ⊆ 𝑦 } ) )