Metamath Proof Explorer

Theorem ist0-2

Description: The predicate "is a T_0 space". (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ist0-2 
|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> 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 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 ist0 
 |-  ( J e. 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 ) ) )
4 3 baib 
 |-  ( J e. Top -> ( J e. Kol2 <-> A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
5 1 4 syl 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 6 raleqdv 
 |-  ( J e. ( TopOn ` X ) -> ( A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
8 6 7 raleqbidv 
 |-  ( J e. ( TopOn ` X ) -> ( A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
9 5 8 bitr4d 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )