Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
2 |
|
eqid |
|- U. J = U. J |
3 |
2
|
ishaus |
|- ( J e. 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 ) = (/) ) ) ) ) |
4 |
3
|
baib |
|- ( J e. Top -> ( J e. Haus <-> 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 ) = (/) ) ) ) ) |
5 |
1 4
|
syl |
|- ( J e. ( TopOn ` X ) -> ( J e. Haus <-> 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 ) = (/) ) ) ) ) |
6 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
7 |
6
|
raleqdv |
|- ( J e. ( TopOn ` 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 ) = (/) ) ) <-> 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 ) = (/) ) ) ) ) |
8 |
6 7
|
raleqbidv |
|- ( J e. ( TopOn ` X ) -> ( 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 ) = (/) ) ) <-> 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 ) = (/) ) ) ) ) |
9 |
5 8
|
bitr4d |
|- ( J e. ( TopOn ` X ) -> ( J e. Haus <-> 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 ) = (/) ) ) ) ) |