# Metamath Proof Explorer

## Theorem ist0

Description: The predicate "is a T_0 space". Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 . (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Hypothesis ist0.1 ${⊢}{X}=\bigcup {J}$
Assertion ist0 ${⊢}{J}\in \mathrm{Kol2}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ist0.1 ${⊢}{X}=\bigcup {J}$
2 unieq ${⊢}{j}={J}\to \bigcup {j}=\bigcup {J}$
3 2 1 eqtr4di ${⊢}{j}={J}\to \bigcup {j}={X}$
4 raleq ${⊢}{j}={J}\to \left(\forall {o}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)↔\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\right)$
5 4 imbi1d ${⊢}{j}={J}\to \left(\left(\forall {o}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)↔\left(\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)\right)$
6 3 5 raleqbidv ${⊢}{j}={J}\to \left(\forall {y}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)\right)$
7 3 6 raleqbidv ${⊢}{j}={J}\to \left(\forall {x}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)\right)$
8 df-t0 ${⊢}\mathrm{Kol2}=\left\{{j}\in \mathrm{Top}|\forall {x}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)\right\}$
9 7 8 elrab2 ${⊢}{J}\in \mathrm{Kol2}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}↔{y}\in {o}\right)\to {x}={y}\right)\right)$