Metamath Proof Explorer

Theorem ishaus2

Description: Express the predicate " J is a Hausdorff space." (Contributed by NM, 8-Mar-2007)

Ref Expression
Assertion ishaus2 
|- ( 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 ) = (/) ) ) ) )

Proof

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 ) = (/) ) ) ) )