Metamath Proof Explorer

Theorem clsfval

Description: The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	cldval.1	$⊢ X = ⋃ J$
	Assertion	clsfval	$⊢ J \in Top \to cls (J) = (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\})$

Proof

Step	Hyp	Ref	Expression
1		cldval.1	$⊢ X = ⋃ J$
2	1	topopn	$⊢ J \in Top \to X \in J$
3		pwexg	$⊢ X \in J \to 𝒫 X \in V$
4		mptexg	$⊢ 𝒫 X \in V \to (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\}) \in V$
5	2 3 4	3syl	$⊢ J \in Top \to (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\}) \in V$
6		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
7	6 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
8	7	pweqd	$⊢ j = J \to 𝒫 ⋃ j = 𝒫 X$
9		fveq2	$⊢ j = J \to Clsd (j) = Clsd (J)$
10	9	rabeqdv	$⊢ j = J \to \{y \in Clsd (j) \| x \subseteq y\} = \{y \in Clsd (J) \| x \subseteq y\}$
11	10	inteqd	$⊢ j = J \to ⋂ \{y \in Clsd (j) \| x \subseteq y\} = ⋂ \{y \in Clsd (J) \| x \subseteq y\}$
12	8 11	mpteq12dv	$⊢ j = J \to (x \in 𝒫 ⋃ j ⟼ ⋂ \{y \in Clsd (j) \| x \subseteq y\}) = (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\})$
13		df-cls	$⊢ cls = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ ⋂ \{y \in Clsd (j) \| x \subseteq y\}))$
14	12 13	fvmptg	$⊢ (J \in Top \land (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\}) \in V) \to cls (J) = (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\})$
15	5 14	mpdan	$⊢ J \in Top \to cls (J) = (x \in 𝒫 X ⟼ ⋂ \{y \in Clsd (J) \| x \subseteq y\})$