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

Metamath Proof Explorer

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