Metamath Proof Explorer

Theorem neif

Description: The neighborhood function is a function from the set of the subsets of the base set of a topology. (Contributed by NM, 12-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Hypothesis	neifval.1	$⊢ X = ⋃ J$
	Assertion	neif	$⊢ J \in Top \to nei (J) Fn 𝒫 X$

Proof

Step	Hyp	Ref	Expression
1		neifval.1	$⊢ X = ⋃ J$
2	1	topopn	$⊢ J \in Top \to X \in J$
3		pwexg	$⊢ X \in J \to 𝒫 X \in V$
4		rabexg	$⊢ 𝒫 X \in V \to \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\} \in V$
5	2 3 4	3syl	$⊢ J \in Top \to \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\} \in V$
6	5	ralrimivw	$⊢ J \in Top \to \forall x \in 𝒫 X \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\} \in V$
7		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)\})$
8	7	fnmpt	$⊢ \forall x \in 𝒫 X \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\} \in V \to (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) Fn 𝒫 X$
9	6 8	syl	$⊢ J \in Top \to (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) Fn 𝒫 X$
10	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)\})$
11	10	fneq1d	$⊢ J \in Top \to (nei (J) Fn 𝒫 X \leftrightarrow (x \in 𝒫 X ⟼ \{v \in 𝒫 X \| \exists g \in J (x \subseteq g \land g \subseteq v)\}) Fn 𝒫 X)$
12	9 11	mpbird	$⊢ J \in Top \to nei (J) Fn 𝒫 X$