Metamath Proof Explorer

Theorem t1sep

Description: Any two distinct points in a T_1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Hypothesis t1sep.1 ⊢ X = ⋃ J
Assertion t1sep ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ∃ o ∈ J A ∈ o ∧ ¬ B ∈ o

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ X = ⋃ J
2 simpr3 ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → A ≠ B
3 1 t1sep2 ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o → B ∈ o → A = B
4 3 3adant3r3 ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ∀ o ∈ J A ∈ o → B ∈ o → A = B
5 4 necon3ad ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → A ≠ B → ¬ ∀ o ∈ J A ∈ o → B ∈ o
6 2 5 mpd ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ¬ ∀ o ∈ J A ∈ o → B ∈ o
7 rexanali ⊢ ∃ o ∈ J A ∈ o ∧ ¬ B ∈ o ↔ ¬ ∀ o ∈ J A ∈ o → B ∈ o
8 6 7 sylibr ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X ∧ A ≠ B → ∃ o ∈ J A ∈ o ∧ ¬ B ∈ o