Metamath Proof Explorer

Theorem isnei

Description: The predicate "the class N is a neighborhood of S ". (Contributed by FL, 25-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis neifval.1 ⊢ X = ⋃ J
Assertion isnei ⊢ J ∈ Top ∧ S ⊆ X → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ X = ⋃ J
2 1 neival ⊢ J ∈ Top ∧ S ⊆ X → nei ⁡ J ⁡ S = v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v
3 2 eleq2d ⊢ J ∈ Top ∧ S ⊆ X → N ∈ nei ⁡ J ⁡ S ↔ N ∈ v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v
4 sseq2 ⊢ v = N → g ⊆ v ↔ g ⊆ N
5 4 anbi2d ⊢ v = N → S ⊆ g ∧ g ⊆ v ↔ S ⊆ g ∧ g ⊆ N
6 5 rexbidv ⊢ v = N → ∃ g ∈ J S ⊆ g ∧ g ⊆ v ↔ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
7 6 elrab ⊢ N ∈ v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v ↔ N ∈ 𝒫 X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
8 1 topopn ⊢ J ∈ Top → X ∈ J
9 elpw2g ⊢ X ∈ J → N ∈ 𝒫 X ↔ N ⊆ X
10 8 9 syl ⊢ J ∈ Top → N ∈ 𝒫 X ↔ N ⊆ X
11 10 anbi1d ⊢ J ∈ Top → N ∈ 𝒫 X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
12 7 11 syl5bb ⊢ J ∈ Top → N ∈ v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
13 12 adantr ⊢ J ∈ Top ∧ S ⊆ X → N ∈ v ∈ 𝒫 X | ∃ g ∈ J S ⊆ g ∧ g ⊆ v ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N
14 3 13 bitrd ⊢ J ∈ Top ∧ S ⊆ X → N ∈ nei ⁡ J ⁡ S ↔ N ⊆ X ∧ ∃ g ∈ J S ⊆ g ∧ g ⊆ N