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 ⊢ X = ⋃ J
Assertion t0sep ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X → ∀ x ∈ J A ∈ x ↔ B ∈ x → A = B

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 1 ist0 ⊢ J ∈ Kol2 ↔ J ∈ Top ∧ ∀ y ∈ X ∀ z ∈ X ∀ x ∈ J y ∈ x ↔ z ∈ x → y = z
3 2 simprbi ⊢ J ∈ Kol2 → ∀ y ∈ X ∀ z ∈ X ∀ x ∈ J y ∈ x ↔ z ∈ x → y = z
4 eleq1 ⊢ y = A → y ∈ x ↔ A ∈ x
5 4 bibi1d ⊢ y = A → y ∈ x ↔ z ∈ x ↔ A ∈ x ↔ z ∈ x
6 5 ralbidv ⊢ y = A → ∀ x ∈ J y ∈ x ↔ z ∈ x ↔ ∀ x ∈ J A ∈ x ↔ z ∈ x
7 eqeq1 ⊢ y = A → y = z ↔ A = z
8 6 7 imbi12d ⊢ y = A → ∀ x ∈ J y ∈ x ↔ z ∈ x → y = z ↔ ∀ x ∈ J A ∈ x ↔ z ∈ x → A = z
9 eleq1 ⊢ z = B → z ∈ x ↔ B ∈ x
10 9 bibi2d ⊢ z = B → A ∈ x ↔ z ∈ x ↔ A ∈ x ↔ B ∈ x
11 10 ralbidv ⊢ z = B → ∀ x ∈ J A ∈ x ↔ z ∈ x ↔ ∀ x ∈ J A ∈ x ↔ B ∈ x
12 eqeq2 ⊢ z = B → A = z ↔ A = B
13 11 12 imbi12d ⊢ z = B → ∀ x ∈ J A ∈ x ↔ z ∈ x → A = z ↔ ∀ x ∈ J A ∈ x ↔ B ∈ x → A = B
14 8 13 rspc2va ⊢ A ∈ X ∧ B ∈ X ∧ ∀ y ∈ X ∀ z ∈ X ∀ x ∈ J y ∈ x ↔ z ∈ x → y = z → ∀ x ∈ J A ∈ x ↔ B ∈ x → A = B
15 14 ancoms ⊢ ∀ y ∈ X ∀ z ∈ X ∀ x ∈ J y ∈ x ↔ z ∈ x → y = z ∧ A ∈ X ∧ B ∈ X → ∀ x ∈ J A ∈ x ↔ B ∈ x → A = B
16 3 15 sylan ⊢ J ∈ Kol2 ∧ A ∈ X ∧ B ∈ X → ∀ x ∈ J A ∈ x ↔ B ∈ x → A = B