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

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

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ 𝑋 = ∪ 𝐽
2 1 t0sep ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )
3 2 necon3ad ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ≠ 𝐵 → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) )
4 3 exp32 ⊢ ( 𝐽 ∈ Kol2 → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 ≠ 𝐵 → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ) ) ) )
5 4 3imp2 ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) )
6 rexnal ⊢ ( ∃ 𝑜 ∈ 𝐽 ¬ ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) )
7 5 6 sylibr ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑜 ∈ 𝐽 ¬ ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) )