# Metamath Proof Explorer

## Theorem ishaus

Description: The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007)

Ref Expression
Hypothesis ist0.1 ${⊢}{X}=\bigcup {J}$
Assertion ishaus ${⊢}{J}\in \mathrm{Haus}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {J}\phantom{\rule{.4em}{0ex}}\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\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 syl6eqr ${⊢}{j}={J}\to \bigcup {j}={X}$
4 rexeq ${⊢}{j}={J}\to \left(\exists {m}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)↔\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)$
5 4 rexeqbi1dv ${⊢}{j}={J}\to \left(\exists {n}\in {j}\phantom{\rule{.4em}{0ex}}\exists {m}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)↔\exists {n}\in {J}\phantom{\rule{.4em}{0ex}}\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)$
6 5 imbi2d ${⊢}{j}={J}\to \left(\left({x}\ne {y}\to \exists {n}\in {j}\phantom{\rule{.4em}{0ex}}\exists {m}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)↔\left({x}\ne {y}\to \exists {n}\in {J}\phantom{\rule{.4em}{0ex}}\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)\right)$
7 3 6 raleqbidv ${⊢}{j}={J}\to \left(\forall {y}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {j}\phantom{\rule{.4em}{0ex}}\exists {m}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {J}\phantom{\rule{.4em}{0ex}}\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)\right)$
8 3 7 raleqbidv ${⊢}{j}={J}\to \left(\forall {x}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {j}\phantom{\rule{.4em}{0ex}}\exists {m}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {J}\phantom{\rule{.4em}{0ex}}\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)\right)$
9 df-haus ${⊢}\mathrm{Haus}=\left\{{j}\in \mathrm{Top}|\forall {x}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcup {j}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {j}\phantom{\rule{.4em}{0ex}}\exists {m}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)\right\}$
10 8 9 elrab2 ${⊢}{J}\in \mathrm{Haus}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to \exists {n}\in {J}\phantom{\rule{.4em}{0ex}}\exists {m}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {n}\wedge {y}\in {m}\wedge {n}\cap {m}=\varnothing \right)\right)\right)$