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∈Xx≠y→∃o∈Jx∈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∈Jx∈o↔y∈o→x=y
2 con34b ⊢∀o∈Jx∈o↔y∈o→x=y↔¬x=y→¬∀o∈Jx∈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∈Jx∈o∧¬y∈o∨¬x∈o∧y∈o
9 rexnal ⊢∃o∈J¬x∈o↔y∈o↔¬∀o∈Jx∈o↔y∈o
10 8 9 bitr3i ⊢∃o∈Jx∈o∧¬y∈o∨¬x∈o∧y∈o↔¬∀o∈Jx∈o↔y∈o
11 3 10 imbi12i ⊢x≠y→∃o∈Jx∈o∧¬y∈o∨¬x∈o∧y∈o↔¬x=y→¬∀o∈Jx∈o↔y∈o
12 2 11 bitr4i ⊢∀o∈Jx∈o↔y∈o→x=y↔x≠y→∃o∈Jx∈o∧¬y∈o∨¬x∈o∧y∈o
13 12 2ralbii ⊢∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y↔∀x∈X∀y∈Xx≠y→∃o∈Jx∈o∧¬y∈o∨¬x∈o∧y∈o
14 1 13 bitrdi ⊢J∈TopOn⁡X→J∈Kol2↔∀x∈X∀y∈Xx≠y→∃o∈Jx∈o∧¬y∈o∨¬x∈o∧y∈o