Definition df-cld 12745

Description: Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)

Assertion

Ref	Expression
df-cld	⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗})

Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-cld

Step	Hyp	Ref	Expression
1		ccld 12742	. 2 class Clsd
2		vj	. . 3 setvar 𝑗
3		ctop 12645	. . 3 class Top
4	2	cv 1342	. . . . . . 7 class 𝑗
5	4	cuni 3789	. . . . . 6 class ∪ 𝑗
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1342	. . . . . 6 class 𝑥
8	5, 7	cdif 3113	. . . . 5 class (∪ 𝑗 ∖ 𝑥)
9	8, 4	wcel 2136	. . . 4 wff (∪ 𝑗 ∖ 𝑥) ∈ 𝑗
10	5	cpw 3559	. . . 4 class 𝒫 ∪ 𝑗
11	9, 6, 10	crab 2448	. . 3 class {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗}
12	2, 3, 11	cmpt 4043	. 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗})
13	1, 12	wceq 1343	1 wff Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗})

This definition is referenced by:  fncld  12748  cldval  12749