clsval

Description: The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure of Munkres p. 94. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	iscld.1	$⊢ X = ⋃ J$
	Assertion	clsval	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$⊢ X = ⋃ J$
2	1	clsfval	$⊢ J \in Top \to cls (J) = (y \in 𝒫 X ⟼ ⋂ \{x \in Clsd (J) \| y \subseteq x\})$
3	2	fveq1d	$⊢ J \in Top \to cls (J) (S) = (y \in 𝒫 X ⟼ ⋂ \{x \in Clsd (J) \| y \subseteq x\}) (S)$
4	3	adantr	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = (y \in 𝒫 X ⟼ ⋂ \{x \in Clsd (J) \| y \subseteq x\}) (S)$
5		eqid	$⊢ (y \in 𝒫 X ⟼ ⋂ \{x \in Clsd (J) \| y \subseteq x\}) = (y \in 𝒫 X ⟼ ⋂ \{x \in Clsd (J) \| y \subseteq x\})$
6		sseq1	$⊢ y = S \to (y \subseteq x \leftrightarrow S \subseteq x)$
7	6	rabbidv	$⊢ y = S \to \{x \in Clsd (J) \| y \subseteq x\} = \{x \in Clsd (J) \| S \subseteq x\}$
8	7	inteqd	$⊢ y = S \to ⋂ \{x \in Clsd (J) \| y \subseteq x\} = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
9	1	topopn	$⊢ J \in Top \to X \in J$
10		elpw2g	$⊢ X \in J \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
11	9 10	syl	$⊢ J \in Top \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
12	11	biimpar	$⊢ (J \in Top \land S \subseteq X) \to S \in 𝒫 X$
13	1	topcld	$⊢ J \in Top \to X \in Clsd (J)$
14		sseq2	$⊢ x = X \to (S \subseteq x \leftrightarrow S \subseteq X)$
15	14	rspcev	$⊢ (X \in Clsd (J) \land S \subseteq X) \to \exists x \in Clsd (J) S \subseteq x$
16	13 15	sylan	$⊢ (J \in Top \land S \subseteq X) \to \exists x \in Clsd (J) S \subseteq x$
17		intexrab	$⊢ \exists x \in Clsd (J) S \subseteq x \leftrightarrow ⋂ \{x \in Clsd (J) \| S \subseteq x\} \in V$
18	16 17	sylib	$⊢ (J \in Top \land S \subseteq X) \to ⋂ \{x \in Clsd (J) \| S \subseteq x\} \in V$
19	5 8 12 18	fvmptd3	$⊢ (J \in Top \land S \subseteq X) \to (y \in 𝒫 X ⟼ ⋂ \{x \in Clsd (J) \| y \subseteq x\}) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
20	4 19	eqtrd	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$

Metamath Proof Explorer

Theorem clsval

Proof