Metamath Proof Explorer


Theorem ist0-3

Description: The predicate "is a T_0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion ist0-3 J TopOn X J Kol2 x X y X x y o J x o ¬ y o ¬ x o y o

Proof

Step Hyp Ref Expression
1 ist0-2 J TopOn X J Kol2 x X y X o J x o y o x = y
2 con34b o J x o y o x = y ¬ x = y ¬ o J x o y o
3 df-ne x y ¬ x = y
4 xor ¬ x o y o x o ¬ y o y o ¬ x o
5 ancom y o ¬ x o ¬ x o y o
6 5 orbi2i x o ¬ y o y o ¬ x o x o ¬ y o ¬ x o y o
7 4 6 bitri ¬ x o y o x o ¬ y o ¬ x o y o
8 7 rexbii o J ¬ x o y o o J x o ¬ y o ¬ x o y o
9 rexnal o J ¬ x o y o ¬ o J x o y o
10 8 9 bitr3i o J x o ¬ y o ¬ x o y o ¬ o J x o y o
11 3 10 imbi12i x y o J x o ¬ y o ¬ x o y o ¬ x = y ¬ o J x o y o
12 2 11 bitr4i o J x o y o x = y x y o J x o ¬ y o ¬ x o y o
13 12 2ralbii x X y X o J x o y o x = y x X y X x y o J x o ¬ y o ¬ x o y o
14 1 13 bitrdi J TopOn X J Kol2 x X y X x y o J x o ¬ y o ¬ x o y o