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