This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
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 𝒫 𝑋 )