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 ∈ Top ∧ S ⊆ X → nei ⁡ J ⁡ S = v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ X = ⋃ J
2 1 neifval ⊢ J ∈ Top → nei ⁡ J = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v
3 2 fveq1d ⊢ J ∈ Top → nei ⁡ J ⁡ S = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v ⁡ S
4 3 adantr ⊢ J ∈ Top ∧ S ⊆ X → nei ⁡ J ⁡ S = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v ⁡ S
5 eqid ⊢ x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v = x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v
6 cleq1lem ⊢ x = S → x ⊆ g ∧ g ⊆ v ↔ S ⊆ g ∧ g ⊆ v
7 6 rexbidv ⊢ x = S → ∃ g ∈ J x ⊆ g ∧ g ⊆ v ↔ ∃ g ∈ J S ⊆ g ∧ g ⊆ v
8 7 rabbidv ⊢ x = S → v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v = v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v
9 1 topopn ⊢ J ∈ Top → X ∈ J
10 elpw2g ⊢ X ∈ J → S ∈ 𝒫 X ↔ S ⊆ X
11 9 10 syl ⊢ J ∈ Top → S ∈ 𝒫 X ↔ S ⊆ X
12 11 biimpar ⊢ J ∈ Top ∧ S ⊆ X → S ∈ 𝒫 X
13 pwexg ⊢ X ∈ J → 𝒫 X ∈ V
14 rabexg ⊢ 𝒫 X ∈ V → v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v ∈ V
15 9 13 14 3syl ⊢ J ∈ Top → v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v ∈ V
16 15 adantr ⊢ J ∈ Top ∧ S ⊆ X → v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v ∈ V
17 5 8 12 16 fvmptd3 ⊢ J ∈ Top ∧ S ⊆ X → x ∈ 𝒫 X ⟼ v ∈ 𝒫 X | ∃ g ∈ J x ⊆ g ∧ g ⊆ v ⁡ S = v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v
18 4 17 eqtrd ⊢ J ∈ Top ∧ S ⊆ X → nei ⁡ J ⁡ S = v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v