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 bitrid 
 |-  ( ( 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 ) )