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 = U. J
Assertion neifg
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( X filGen { x e. J | S C_ x } ) = ( ( nei ` J ) ` S ) )

Proof

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