Metamath Proof Explorer

Theorem t0sep

Description: Any two topologically indistinguishable points in a T_0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis ist0.1 𝑋 = 𝐽
Assertion t0sep ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ∀ 𝑥𝐽 ( 𝐴𝑥𝐵𝑥 ) → 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ist0.1 𝑋 = 𝐽
2 1 ist0 ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦𝑋𝑧𝑋 ( ∀ 𝑥𝐽 ( 𝑦𝑥𝑧𝑥 ) → 𝑦 = 𝑧 ) ) )
3 2 simprbi ( 𝐽 ∈ Kol2 → ∀ 𝑦𝑋𝑧𝑋 ( ∀ 𝑥𝐽 ( 𝑦𝑥𝑧𝑥 ) → 𝑦 = 𝑧 ) )
4 eleq1 ( 𝑦 = 𝐴 → ( 𝑦𝑥𝐴𝑥 ) )
5 4 bibi1d ( 𝑦 = 𝐴 → ( ( 𝑦𝑥𝑧𝑥 ) ↔ ( 𝐴𝑥𝑧𝑥 ) ) )
6 5 ralbidv ( 𝑦 = 𝐴 → ( ∀ 𝑥𝐽 ( 𝑦𝑥𝑧𝑥 ) ↔ ∀ 𝑥𝐽 ( 𝐴𝑥𝑧𝑥 ) ) )
7 eqeq1 ( 𝑦 = 𝐴 → ( 𝑦 = 𝑧𝐴 = 𝑧 ) )
8 6 7 imbi12d ( 𝑦 = 𝐴 → ( ( ∀ 𝑥𝐽 ( 𝑦𝑥𝑧𝑥 ) → 𝑦 = 𝑧 ) ↔ ( ∀ 𝑥𝐽 ( 𝐴𝑥𝑧𝑥 ) → 𝐴 = 𝑧 ) ) )
9 eleq1 ( 𝑧 = 𝐵 → ( 𝑧𝑥𝐵𝑥 ) )
10 9 bibi2d ( 𝑧 = 𝐵 → ( ( 𝐴𝑥𝑧𝑥 ) ↔ ( 𝐴𝑥𝐵𝑥 ) ) )
11 10 ralbidv ( 𝑧 = 𝐵 → ( ∀ 𝑥𝐽 ( 𝐴𝑥𝑧𝑥 ) ↔ ∀ 𝑥𝐽 ( 𝐴𝑥𝐵𝑥 ) ) )
12 eqeq2 ( 𝑧 = 𝐵 → ( 𝐴 = 𝑧𝐴 = 𝐵 ) )
13 11 12 imbi12d ( 𝑧 = 𝐵 → ( ( ∀ 𝑥𝐽 ( 𝐴𝑥𝑧𝑥 ) → 𝐴 = 𝑧 ) ↔ ( ∀ 𝑥𝐽 ( 𝐴𝑥𝐵𝑥 ) → 𝐴 = 𝐵 ) ) )
14 8 13 rspc2va ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ∀ 𝑦𝑋𝑧𝑋 ( ∀ 𝑥𝐽 ( 𝑦𝑥𝑧𝑥 ) → 𝑦 = 𝑧 ) ) → ( ∀ 𝑥𝐽 ( 𝐴𝑥𝐵𝑥 ) → 𝐴 = 𝐵 ) )
15 14 ancoms ( ( ∀ 𝑦𝑋𝑧𝑋 ( ∀ 𝑥𝐽 ( 𝑦𝑥𝑧𝑥 ) → 𝑦 = 𝑧 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ∀ 𝑥𝐽 ( 𝐴𝑥𝐵𝑥 ) → 𝐴 = 𝐵 ) )
16 3 15 sylan ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ∀ 𝑥𝐽 ( 𝐴𝑥𝐵𝑥 ) → 𝐴 = 𝐵 ) )