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