Theorem ishaus

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

	Ref	Expression
Hypothesis	ist0.1	|- X = U. J
Assertion	ishaus	|- ( 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 ) = (/) ) ) ) )

Proof

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