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

Metamath Proof Explorer

Theorem islly

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

Ref Expression
Assertion islly 
|- ( J e. Locally A <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 
 |-  ( j = J -> ( j i^i ~P x ) = ( J i^i ~P x ) )
2 oveq1 
 |-  ( j = J -> ( j |`t u ) = ( J |`t u ) )
3 2 eleq1d 
 |-  ( j = J -> ( ( j |`t u ) e. A <-> ( J |`t u ) e. A ) )
4 3 anbi2d 
 |-  ( j = J -> ( ( y e. u /\ ( j |`t u ) e. A ) <-> ( y e. u /\ ( J |`t u ) e. A ) ) )
5 1 4 rexeqbidv 
 |-  ( j = J -> ( E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) <-> E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) ) )
6 5 ralbidv 
 |-  ( j = J -> ( A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) <-> A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) ) )
7 6 raleqbi1dv 
 |-  ( j = J -> ( A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) <-> A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) ) )
8 df-lly 
 |-  Locally A = { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) }
9 7 8 elrab2 
 |-  ( J e. Locally A <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. A ) ) )