This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ist0

Description: The predicate "is a T_0 space". Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 . (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Hypothesis ist0.1 
|- X = U. J
Assertion ist0 
|- ( J e. Kol2 <-> ( J e. Top /\ A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )

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 raleq 
 |-  ( j = J -> ( A. o e. j ( x e. o <-> y e. o ) <-> A. o e. J ( x e. o <-> y e. o ) ) )
5 4 imbi1d 
 |-  ( j = J -> ( ( A. o e. j ( x e. o <-> y e. o ) -> x = y ) <-> ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
6 3 5 raleqbidv 
 |-  ( j = J -> ( A. y e. U. j ( A. o e. j ( x e. o <-> y e. o ) -> x = y ) <-> A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
7 3 6 raleqbidv 
 |-  ( j = J -> ( A. x e. U. j A. y e. U. j ( A. o e. j ( x e. o <-> y e. o ) -> x = y ) <-> A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
8 df-t0 
 |-  Kol2 = { j e. Top | A. x e. U. j A. y e. U. j ( A. o e. j ( x e. o <-> y e. o ) -> x = y ) }
9 7 8 elrab2 
 |-  ( J e. Kol2 <-> ( J e. Top /\ A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )