Metamath Proof Explorer

Theorem neival

Description: Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	neifval.1	$⊢ X = ⋃ J$
	Assertion	neival	$⊢ (J \in Top \land S \subseteq X) \to nei (J) (S) = \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\}$

Proof

Step	Hyp	Ref	Expression
1		neifval.1	$⊢ X = ⋃ J$
2	1	neifval	$⊢ J \in Top \to nei (J) = (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\})$
3	2	fveq1d	$⊢ J \in Top \to nei (J) (S) = (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) (S)$
4	3	adantr	$⊢ (J \in Top \land S \subseteq X) \to nei (J) (S) = (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) (S)$
5		eqid	$⊢ (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) = (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\})$
6		cleq1lem	$⊢ x = S \to ((x \subseteq g \land g \subseteq v) \leftrightarrow (S \subseteq g \land g \subseteq v))$
7	6	rexbidv	$⊢ x = S \to (\exists g \in J (x \subseteq g \land g \subseteq v) \leftrightarrow \exists g \in J (S \subseteq g \land g \subseteq v))$
8	7	rabbidv	$⊢ x = S \to \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\} = \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\}$
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		pwexg	$⊢ X \in J \to 𝒫 X \in V$
14		rabexg	$⊢ 𝒫 X \in V \to \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\} \in V$
15	9 13 14	3syl	$⊢ J \in Top \to \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\} \in V$
16	15	adantr	$⊢ (J \in Top \land S \subseteq X) \to \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\} \in V$
17	5 8 12 16	fvmptd3	$⊢ (J \in Top \land S \subseteq X) \to (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) (S) = \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\}$
18	4 17	eqtrd	$⊢ (J \in Top \land S \subseteq X) \to nei (J) (S) = \{v \in 𝒫 X \| \exists g \in J (S \subseteq g \land g \subseteq v)\}$