Metamath Proof Explorer

Theorem isnlly

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

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( j = J -> ( nei ` j ) = ( nei ` J ) )
2 1 fveq1d 
 |-  ( j = J -> ( ( nei ` j ) ` { y } ) = ( ( nei ` J ) ` { y } ) )
3 2 ineq1d 
 |-  ( j = J -> ( ( ( nei ` j ) ` { y } ) i^i ~P x ) = ( ( ( nei ` J ) ` { y } ) i^i ~P x ) )
4 oveq1 
 |-  ( j = J -> ( j |`t u ) = ( J |`t u ) )
5 4 eleq1d 
 |-  ( j = J -> ( ( j |`t u ) e. A <-> ( J |`t u ) e. A ) )
6 3 5 rexeqbidv 
 |-  ( j = J -> ( E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A <-> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A ) )
7 6 ralbidv 
 |-  ( j = J -> ( A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A <-> A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A ) )
8 7 raleqbi1dv 
 |-  ( j = J -> ( A. x e. j A. y e. x E. u e. ( ( ( nei ` j ) ` { y } ) i^i ~P x ) ( j |`t u ) e. A <-> A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A ) )
9 df-nlly 
 |-  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 }
10 8 9 elrab2 
 |-  ( 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 ) )