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 = J
Assertion ist0 J Kol2 J Top x X y X o J x o y o x = y

Proof

Step Hyp Ref Expression
1 ist0.1 X = J
2 unieq j = J j = J
3 2 1 eqtr4di j = J j = X
4 raleq j = J o j x o y o o J x o y o
5 4 imbi1d j = J o j x o y o x = y o J x o y o x = y
6 3 5 raleqbidv j = J y j o j x o y o x = y y X o J x o y o x = y
7 3 6 raleqbidv j = J x j y j o j x o y o x = y x X y X o J x o y o x = y
8 df-t0 Kol2 = j Top | x j y j o j x o y o x = y
9 7 8 elrab2 J Kol2 J Top x X y X o J x o y o x = y