Metamath Proof Explorer


Theorem t0hmph

Description: T_0 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion t0hmph JKJKol2KKol2

Proof

Step Hyp Ref Expression
1 t0top JKol2JTop
2 cnt0 JKol2f:K1-1JfKCnJKKol2
3 1 2 haushmphlem JKJKol2KKol2