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 = (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| ⋃ j ∖ x \in j\})$

Step	Hyp	Ref	Expression
0		ccld	$class Clsd$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6	5	cpw	$class 𝒫 ⋃ j$
7	3	cv	$setvar x$
8	5 7	cdif	$class (⋃ j ∖ x)$
9	8 4	wcel	$wff ⋃ j ∖ x \in j$
10	9 3 6	crab	$class \{x \in 𝒫 ⋃ j \| ⋃ j ∖ x \in j\}$
11	1 2 10	cmpt	$class (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| ⋃ j ∖ x \in j\})$
12	0 11	wceq	$wff Clsd = (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| ⋃ j ∖ x \in j\})$

Metamath Proof Explorer