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	⊢ 𝑋 = ∪ 𝐽
Assertion	neif	⊢ ( 𝐽 ∈ Top → ( nei ‘ 𝐽 ) Fn 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		neifval.1	⊢ 𝑋 = ∪ 𝐽
2	1	topopn	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
3		pwexg	⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V )
4		rabexg	⊢ ( 𝒫 𝑋 ∈ V → { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V )
5	2 3 4	3syl	⊢ ( 𝐽 ∈ Top → { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V )
6	5	ralrimivw	⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ∈ 𝒫 𝑋 { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V )
7		eqid	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } )
8	7	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝒫 𝑋 { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ∈ V → ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) Fn 𝒫 𝑋 )
9	6 8	syl	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) Fn 𝒫 𝑋 )
10	1	neifval	⊢ ( 𝐽 ∈ Top → ( nei ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) )
11	10	fneq1d	⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) Fn 𝒫 𝑋 ↔ ( 𝑥 ∈ 𝒫 𝑋 ↦ { 𝑣 ∈ 𝒫 𝑋 ∣ ∃ 𝑔 ∈ 𝐽 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣 ) } ) Fn 𝒫 𝑋 ) )
12	9 11	mpbird	⊢ ( 𝐽 ∈ Top → ( nei ‘ 𝐽 ) Fn 𝒫 𝑋 )