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