Metamath Proof Explorer


Theorem neifg

Description: The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas . (Contributed by Jeff Hankins, 3-Sep-2009)

Ref Expression
Hypothesis neifg.1 X = J
Assertion neifg J Top S X S X filGen x J | S x = nei J S

Proof

Step Hyp Ref Expression
1 neifg.1 X = J
2 1 opnfbas J Top S X S x J | S x fBas X
3 fgval x J | S x fBas X X filGen x J | S x = t 𝒫 X | x J | S x 𝒫 t
4 2 3 syl J Top S X S X filGen x J | S x = t 𝒫 X | x J | S x 𝒫 t
5 pweq t = u 𝒫 t = 𝒫 u
6 5 ineq2d t = u x J | S x 𝒫 t = x J | S x 𝒫 u
7 6 neeq1d t = u x J | S x 𝒫 t x J | S x 𝒫 u
8 7 elrab u t 𝒫 X | x J | S x 𝒫 t u 𝒫 X x J | S x 𝒫 u
9 velpw u 𝒫 X u X
10 9 a1i J Top S X S u 𝒫 X u X
11 n0 x J | S x 𝒫 u z z x J | S x 𝒫 u
12 elin z x J | S x 𝒫 u z x J | S x z 𝒫 u
13 sseq2 x = z S x S z
14 13 elrab z x J | S x z J S z
15 velpw z 𝒫 u z u
16 14 15 anbi12i z x J | S x z 𝒫 u z J S z z u
17 12 16 bitri z x J | S x 𝒫 u z J S z z u
18 17 exbii z z x J | S x 𝒫 u z z J S z z u
19 11 18 bitri x J | S x 𝒫 u z z J S z z u
20 19 a1i J Top S X S x J | S x 𝒫 u z z J S z z u
21 10 20 anbi12d J Top S X S u 𝒫 X x J | S x 𝒫 u u X z z J S z z u
22 anass z J S z z u z J S z z u
23 22 exbii z z J S z z u z z J S z z u
24 df-rex z J S z z u z z J S z z u
25 23 24 bitr4i z z J S z z u z J S z z u
26 25 anbi2i u X z z J S z z u u X z J S z z u
27 1 isnei J Top S X u nei J S u X z J S z z u
28 27 3adant3 J Top S X S u nei J S u X z J S z z u
29 26 28 bitr4id J Top S X S u X z z J S z z u u nei J S
30 21 29 bitrd J Top S X S u 𝒫 X x J | S x 𝒫 u u nei J S
31 8 30 syl5bb J Top S X S u t 𝒫 X | x J | S x 𝒫 t u nei J S
32 31 eqrdv J Top S X S t 𝒫 X | x J | S x 𝒫 t = nei J S
33 4 32 eqtrd J Top S X S X filGen x J | S x = nei J S