Metamath Proof Explorer

Theorem t1t0

Description: A T_1 space is a T_0 space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion t1t0 
|- ( J e. Fre -> J e. Kol2 )

Proof

Step Hyp Ref Expression
1 t1top 
 |-  ( J e. Fre -> J e. Top )
2 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
3 1 2 sylib 
 |-  ( J e. Fre -> J e. ( TopOn ` U. J ) )
4 biimp 
 |-  ( ( x e. o <-> y e. o ) -> ( x e. o -> y e. o ) )
5 4 ralimi 
 |-  ( A. o e. J ( x e. o <-> y e. o ) -> A. o e. J ( x e. o -> y e. o ) )
6 5 imim1i 
 |-  ( ( A. o e. J ( x e. o -> y e. o ) -> x = y ) -> ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) )
7 6 ralimi 
 |-  ( A. y e. U. J ( 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 7 ralimi 
 |-  ( 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. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) )
9 8 a1i 
 |-  ( J e. ( TopOn ` U. 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. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
10 ist1-2 
 |-  ( J e. ( TopOn ` U. J ) -> ( J e. Fre <-> A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
11 ist0-2 
 |-  ( J e. ( TopOn ` U. J ) -> ( 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 ) ) )
12 9 10 11 3imtr4d 
 |-  ( J e. ( TopOn ` U. J ) -> ( J e. Fre -> J e. Kol2 ) )
13 3 12 mpcom 
 |-  ( J e. Fre -> J e. Kol2 )