This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isneip

Description: The predicate "the class N is a neighborhood of point P ". (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis neifval.1 
|- X = U. J
Assertion isneip 
|- ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )

Proof

Step Hyp Ref Expression
1 neifval.1 
 |-  X = U. J
2 snssi 
 |-  ( P e. X -> { P } C_ X )
3 1 isnei 
 |-  ( ( J e. Top /\ { P } C_ X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( { P } C_ g /\ g C_ N ) ) ) )
4 2 3 sylan2 
 |-  ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( { P } C_ g /\ g C_ N ) ) ) )
5 snssg 
 |-  ( P e. X -> ( P e. g <-> { P } C_ g ) )
6 5 anbi1d 
 |-  ( P e. X -> ( ( P e. g /\ g C_ N ) <-> ( { P } C_ g /\ g C_ N ) ) )
7 6 rexbidv 
 |-  ( P e. X -> ( E. g e. J ( P e. g /\ g C_ N ) <-> E. g e. J ( { P } C_ g /\ g C_ N ) ) )
8 7 anbi2d 
 |-  ( P e. X -> ( ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) <-> ( N C_ X /\ E. g e. J ( { P } C_ g /\ g C_ N ) ) ) )
9 8 adantl 
 |-  ( ( J e. Top /\ P e. X ) -> ( ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) <-> ( N C_ X /\ E. g e. J ( { P } C_ g /\ g C_ N ) ) ) )
10 4 9 bitr4d 
 |-  ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )