| 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 |
|
rexeq |
|- ( j = J -> ( E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) |
| 5 |
4
|
rexeqbi1dv |
|- ( j = J -> ( E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) <-> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) |
| 6 |
5
|
imbi2d |
|- ( j = J -> ( ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 7 |
3 6
|
raleqbidv |
|- ( j = J -> ( A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 8 |
3 7
|
raleqbidv |
|- ( j = J -> ( A. x e. U. j A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) <-> A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |
| 9 |
|
df-haus |
|- Haus = { j e. Top | A. x e. U. j A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) } |
| 10 |
8 9
|
elrab2 |
|- ( J e. Haus <-> ( J e. Top /\ A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |