Theorem isnei

Description: The predicate "the class N is a neighborhood of S ". (Contributed by FL, 25-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		neifval.1	|- X = U. J
2	1	neival	|- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
3	2	eleq2d	|- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } ) )
4		sseq2	|- ( v = N -> ( g C_ v <-> g C_ N ) )
5	4	anbi2d	|- ( v = N -> ( ( S C_ g /\ g C_ v ) <-> ( S C_ g /\ g C_ N ) ) )
6	5	rexbidv	|- ( v = N -> ( E. g e. J ( S C_ g /\ g C_ v ) <-> E. g e. J ( S C_ g /\ g C_ N ) ) )
7	6	elrab	|- ( N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } <-> ( N e. ~P X /\ E. g e. J ( S C_ g /\ g C_ N ) ) )
8	1	topopn	|- ( J e. Top -> X e. J )
9		elpw2g	|- ( X e. J -> ( N e. ~P X <-> N C_ X ) )
10	8 9	syl	|- ( J e. Top -> ( N e. ~P X <-> N C_ X ) )
11	10	anbi1d	|- ( J e. Top -> ( ( N e. ~P X /\ E. g e. J ( S C_ g /\ g C_ N ) ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
12	7 11	syl5bb	|- ( J e. Top -> ( N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
13	12	adantr	|- ( ( J e. Top /\ S C_ X ) -> ( N e. { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
14	3 13	bitrd	|- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )