Step |
Hyp |
Ref |
Expression |
1 |
|
ist0.1 |
|- X = U. J |
2 |
|
unieq |
|- ( j = J -> U. j = U. J ) |
3 |
2 1
|
eqtr4di |
|- ( j = J -> U. j = X ) |
4 |
3
|
pweqd |
|- ( j = J -> ~P U. j = ~P X ) |
5 |
|
oveq1 |
|- ( j = J -> ( j |`t x ) = ( J |`t x ) ) |
6 |
5
|
eleq1d |
|- ( j = J -> ( ( j |`t x ) e. Nrm <-> ( J |`t x ) e. Nrm ) ) |
7 |
4 6
|
raleqbidv |
|- ( j = J -> ( A. x e. ~P U. j ( j |`t x ) e. Nrm <-> A. x e. ~P X ( J |`t x ) e. Nrm ) ) |
8 |
|
df-cnrm |
|- CNrm = { j e. Top | A. x e. ~P U. j ( j |`t x ) e. Nrm } |
9 |
7 8
|
elrab2 |
|- ( J e. CNrm <-> ( J e. Top /\ A. x e. ~P X ( J |`t x ) e. Nrm ) ) |