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∈JS⊆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∈JS⊆g∧g⊆v
3 2 eleq2d ⊢J∈Top∧S⊆X→N∈nei⁡J⁡S↔N∈v∈𝒫X|∃g∈JS⊆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∈JS⊆g∧g⊆v↔∃g∈JS⊆g∧g⊆N
7 6 elrab ⊢N∈v∈𝒫X|∃g∈JS⊆g∧g⊆v↔N∈𝒫X∧∃g∈JS⊆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∈JS⊆g∧g⊆N↔N⊆X∧∃g∈JS⊆g∧g⊆N
12 7 11 bitrid ⊢J∈Top→N∈v∈𝒫X|∃g∈JS⊆g∧g⊆v↔N⊆X∧∃g∈JS⊆g∧g⊆N
13 12 adantr ⊢J∈Top∧S⊆X→N∈v∈𝒫X|∃g∈JS⊆g∧g⊆v↔N⊆X∧∃g∈JS⊆g∧g⊆N
14 3 13 bitrd ⊢J∈Top∧S⊆X→N∈nei⁡J⁡S↔N⊆X∧∃g∈JS⊆g∧g⊆N