clsf

Description: The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	clsf	$⊢ J \in Top \to cls (J) : 𝒫 X ⟶ Clsd (J)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
3	1	clsval	$⊢ (J \in Top \land x \subseteq X) \to cls (J) (x) = ⋂ \{y \in Clsd (J) \| x \subseteq y\}$
4		fvex	$⊢ cls (J) (x) \in V$
5	3 4	eqeltrrdi	$⊢ (J \in Top \land x \subseteq X) \to ⋂ \{y \in Clsd (J) \| x \subseteq y\} \in V$
6	2 5	sylan2	$⊢ (J \in Top \land x \in 𝒫 X) \to ⋂ \{y \in Clsd (J) \| x \subseteq y\} \in V$
7	1	clsfval	$⊢ J \in Top \to cls (J) = (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\})$
8		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
9	1	clscld	$⊢ (J \in Top \land y \subseteq X) \to cls (J) (y) \in Clsd (J)$
10	8 9	sylan2	$⊢ (J \in Top \land y \in 𝒫 X) \to cls (J) (y) \in Clsd (J)$
11	6 7 10	fmpt2d	$⊢ J \in Top \to cls (J) : 𝒫 X ⟶ Clsd (J)$

Metamath Proof Explorer