Metamath Proof Explorer

Theorem t0dist

Description: Any two distinct points in a T_0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Hypothesis ist0.1 ⊢ X = ⋃ J
Assertion t0dist ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ∃ o ∈ J ¬ A ∈ o ↔ B ∈ o

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 1 t0sep ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o ↔ B ∈ o → A = B
3 2 necon3ad ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X → A ≠ B → ¬ ∀ o ∈ J A ∈ o ↔ B ∈ o
4 3 exp32 ⊢ J ∈ Kol2 → A ∈ X → B ∈ X → A ≠ B → ¬ ∀ o ∈ J A ∈ o ↔ B ∈ o
5 4 3imp2 ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ¬ ∀ o ∈ J A ∈ o ↔ B ∈ o
6 rexnal ⊢ ∃ o ∈ J ¬ A ∈ o ↔ B ∈ o ↔ ¬ ∀ o ∈ J A ∈ o ↔ B ∈ o
7 5 6 sylibr ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ∃ o ∈ J ¬ A ∈ o ↔ B ∈ o