This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion t1sep ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜 ) )

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ 𝑋 = ∪ 𝐽
2 simpr3 ⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ≠ 𝐵 )
3 1 t1sep2 ⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )
4 3 3adant3r3 ⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )
5 4 necon3ad ⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 ≠ 𝐵 → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) )
6 2 5 mpd ⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) )
7 rexanali ⊢ ( ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜 ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) )
8 6 7 sylibr ⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜 ) )