Metamath Proof Explorer

Theorem neifval

Description: Value of the neighborhood function on the subsets 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 neifval ⊢ J ∈ Top → nei ⁡ J = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ X = ⋃ J
2 1 topopn ⊢ J ∈ Top → X ∈ J
3 pwexg ⊢ X ∈ J → 𝒫 X ∈ V
4 mptexg ⊢ 𝒫 X ∈ V → x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v ∈ V
5 2 3 4 3syl ⊢ J ∈ Top → x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v ∈ V
6 unieq ⊢ j = J → ⋃ j = ⋃ J
7 6 1 eqtr4di ⊢ j = J → ⋃ j = X
8 7 pweqd ⊢ j = J → 𝒫 ⋃ j = 𝒫 X
9 rexeq ⊢ j = J → ∃ g ∈ j x ⊆ g ∧ g ⊆ v ↔ ∃ g ∈ J x ⊆ g ∧ g ⊆ v
10 8 9 rabeqbidv ⊢ j = J → v ∈ 𝒫 ⋃ j | ∃ g ∈ j x ⊆ g ∧ g ⊆ v = v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v
11 8 10 mpteq12dv ⊢ j = J → x ∈ 𝒫 ⋃ j ⟼ v ∈ 𝒫 ⋃ j | ∃ g ∈ j x ⊆ g ∧ g ⊆ v = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v
12 df-nei ⊢ nei = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ v ∈ 𝒫 ⋃ j | ∃ g ∈ j x ⊆ g ∧ g ⊆ v
13 11 12 fvmptg ⊢ J ∈ Top ∧ x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v ∈ V → nei ⁡ J = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v
14 5 13 mpdan ⊢ J ∈ Top → nei ⁡ J = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v