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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑜 ∈ 𝐽 ¬ ( 𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) )