Theorem nllyi

Description: The property of an n-locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	nllyi	|- ( ( J e. N-Locally A /\ U e. J /\ P e. U ) -> E. u e. ( ( nei ` J ) ` { P } ) ( u C_ U /\ ( J |`t u ) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		isnlly	|- ( J e. N-Locally A <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A ) )
2	1	simprbi	|- ( J e. N-Locally A -> A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A )
3		pweq	|- ( x = U -> ~P x = ~P U )
4	3	ineq2d	|- ( x = U -> ( ( ( nei ` J ) ` { y } ) i^i ~P x ) = ( ( ( nei ` J ) ` { y } ) i^i ~P U ) )
5	4	rexeqdv	|- ( x = U -> ( E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A <-> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) ( J |`t u ) e. A ) )
6	5	raleqbi1dv	|- ( x = U -> ( A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A <-> A. y e. U E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) ( J |`t u ) e. A ) )
7	6	rspccva	|- ( ( A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A /\ U e. J ) -> A. y e. U E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) ( J |`t u ) e. A )
8	2 7	sylan	|- ( ( J e. N-Locally A /\ U e. J ) -> A. y e. U E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) ( J |`t u ) e. A )
9		elin	|- ( u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) <-> ( u e. ( ( nei ` J ) ` { y } ) /\ u e. ~P U ) )
10		sneq	|- ( y = P -> { y } = { P } )
11	10	fveq2d	|- ( y = P -> ( ( nei ` J ) ` { y } ) = ( ( nei ` J ) ` { P } ) )
12	11	eleq2d	|- ( y = P -> ( u e. ( ( nei ` J ) ` { y } ) <-> u e. ( ( nei ` J ) ` { P } ) ) )
13		velpw	|- ( u e. ~P U <-> u C_ U )
14	13	a1i	|- ( y = P -> ( u e. ~P U <-> u C_ U ) )
15	12 14	anbi12d	|- ( y = P -> ( ( u e. ( ( nei ` J ) ` { y } ) /\ u e. ~P U ) <-> ( u e. ( ( nei ` J ) ` { P } ) /\ u C_ U ) ) )
16	9 15	syl5bb	|- ( y = P -> ( u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) <-> ( u e. ( ( nei ` J ) ` { P } ) /\ u C_ U ) ) )
17	16	anbi1d	|- ( y = P -> ( ( u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) /\ ( J |`t u ) e. A ) <-> ( ( u e. ( ( nei ` J ) ` { P } ) /\ u C_ U ) /\ ( J |`t u ) e. A ) ) )
18		anass	|- ( ( ( u e. ( ( nei ` J ) ` { P } ) /\ u C_ U ) /\ ( J |`t u ) e. A ) <-> ( u e. ( ( nei ` J ) ` { P } ) /\ ( u C_ U /\ ( J |`t u ) e. A ) ) )
19	17 18	bitrdi	|- ( y = P -> ( ( u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) /\ ( J |`t u ) e. A ) <-> ( u e. ( ( nei ` J ) ` { P } ) /\ ( u C_ U /\ ( J |`t u ) e. A ) ) ) )
20	19	rexbidv2	|- ( y = P -> ( E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) ( J |`t u ) e. A <-> E. u e. ( ( nei ` J ) ` { P } ) ( u C_ U /\ ( J |`t u ) e. A ) ) )
21	20	rspccva	|- ( ( A. y e. U E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P U ) ( J |`t u ) e. A /\ P e. U ) -> E. u e. ( ( nei ` J ) ` { P } ) ( u C_ U /\ ( J |`t u ) e. A ) )
22	8 21	stoic3	|- ( ( J e. N-Locally A /\ U e. J /\ P e. U ) -> E. u e. ( ( nei ` J ) ` { P } ) ( u C_ U /\ ( J |`t u ) e. A ) )