Step |
Hyp |
Ref |
Expression |
1 |
|
ist0.1 |
|- X = U. J |
2 |
|
unieq |
|- ( x = J -> U. x = U. J ) |
3 |
2 1
|
eqtr4di |
|- ( x = J -> U. x = X ) |
4 |
|
fveq2 |
|- ( x = J -> ( Clsd ` x ) = ( Clsd ` J ) ) |
5 |
4
|
eleq2d |
|- ( x = J -> ( { a } e. ( Clsd ` x ) <-> { a } e. ( Clsd ` J ) ) ) |
6 |
3 5
|
raleqbidv |
|- ( x = J -> ( A. a e. U. x { a } e. ( Clsd ` x ) <-> A. a e. X { a } e. ( Clsd ` J ) ) ) |
7 |
|
df-t1 |
|- Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) } |
8 |
6 7
|
elrab2 |
|- ( J e. Fre <-> ( J e. Top /\ A. a e. X { a } e. ( Clsd ` J ) ) ) |