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∈JA∈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∈Jy∈x↔z∈x→y=z
3 2 simprbi ⊢J∈Kol2→∀y∈X∀z∈X∀x∈Jy∈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∈Jy∈x↔z∈x↔∀x∈JA∈x↔z∈x
7 eqeq1 ⊢y=A→y=z↔A=z
8 6 7 imbi12d ⊢y=A→∀x∈Jy∈x↔z∈x→y=z↔∀x∈JA∈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∈JA∈x↔z∈x↔∀x∈JA∈x↔B∈x
12 eqeq2 ⊢z=B→A=z↔A=B
13 11 12 imbi12d ⊢z=B→∀x∈JA∈x↔z∈x→A=z↔∀x∈JA∈x↔B∈x→A=B
14 8 13 rspc2va ⊢A∈X∧B∈X∧∀y∈X∀z∈X∀x∈Jy∈x↔z∈x→y=z→∀x∈JA∈x↔B∈x→A=B
15 14 ancoms ⊢∀y∈X∀z∈X∀x∈Jy∈x↔z∈x→y=z∧A∈X∧B∈X→∀x∈JA∈x↔B∈x→A=B
16 3 15 sylan ⊢J∈Kol2∧A∈X∧B∈X→∀x∈JA∈x↔B∈x→A=B