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 ) ) )