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