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

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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) → 𝐴 = 𝐵 ) )