# 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}=\bigcup {J}$
Assertion t0sep ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{B}\in {x}\right)\to {A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 ist0.1 ${⊢}{X}=\bigcup {J}$
2 1 ist0 ${⊢}{J}\in \mathrm{Kol2}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{z}\in {x}\right)\to {y}={z}\right)\right)$
3 2 simprbi ${⊢}{J}\in \mathrm{Kol2}\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{z}\in {x}\right)\to {y}={z}\right)$
4 eleq1 ${⊢}{y}={A}\to \left({y}\in {x}↔{A}\in {x}\right)$
5 4 bibi1d ${⊢}{y}={A}\to \left(\left({y}\in {x}↔{z}\in {x}\right)↔\left({A}\in {x}↔{z}\in {x}\right)\right)$
6 5 ralbidv ${⊢}{y}={A}\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{z}\in {x}\right)↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{z}\in {x}\right)\right)$
7 eqeq1 ${⊢}{y}={A}\to \left({y}={z}↔{A}={z}\right)$
8 6 7 imbi12d ${⊢}{y}={A}\to \left(\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{z}\in {x}\right)\to {y}={z}\right)↔\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{z}\in {x}\right)\to {A}={z}\right)\right)$
9 eleq1 ${⊢}{z}={B}\to \left({z}\in {x}↔{B}\in {x}\right)$
10 9 bibi2d ${⊢}{z}={B}\to \left(\left({A}\in {x}↔{z}\in {x}\right)↔\left({A}\in {x}↔{B}\in {x}\right)\right)$
11 10 ralbidv ${⊢}{z}={B}\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{z}\in {x}\right)↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{B}\in {x}\right)\right)$
12 eqeq2 ${⊢}{z}={B}\to \left({A}={z}↔{A}={B}\right)$
13 11 12 imbi12d ${⊢}{z}={B}\to \left(\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{z}\in {x}\right)\to {A}={z}\right)↔\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{B}\in {x}\right)\to {A}={B}\right)\right)$
14 8 13 rspc2va ${⊢}\left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{z}\in {x}\right)\to {y}={z}\right)\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{B}\in {x}\right)\to {A}={B}\right)$
15 14 ancoms ${⊢}\left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{z}\in {x}\right)\to {y}={z}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{B}\in {x}\right)\to {A}={B}\right)$
16 3 15 sylan ${⊢}\left({J}\in \mathrm{Kol2}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}↔{B}\in {x}\right)\to {A}={B}\right)$