# Metamath Proof Explorer

## Theorem hausdiag

Description: A topology is Hausdorff iff the diagonal set is closed in the topology's product with itself.EDITORIAL: very clumsy proof, can probably be shortened substantially. (Contributed by Stefan O'Rear, 25-Jan-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypothesis hausdiag.x ${⊢}{X}=\bigcup {J}$
Assertion hausdiag ${⊢}{J}\in \mathrm{Haus}↔\left({J}\in \mathrm{Top}\wedge {\mathrm{I}↾}_{{X}}\in \mathrm{Clsd}\left({J}{×}_{t}{J}\right)\right)$

### Proof

Step Hyp Ref Expression
1 hausdiag.x ${⊢}{X}=\bigcup {J}$
2 1 ishaus ${⊢}{J}\in \mathrm{Haus}↔\left({J}\in \mathrm{Top}\wedge \forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)\right)$
3 txtop ${⊢}\left({J}\in \mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
4 3 anidms ${⊢}{J}\in \mathrm{Top}\to {J}{×}_{t}{J}\in \mathrm{Top}$
5 idssxp ${⊢}{\mathrm{I}↾}_{{X}}\subseteq {X}×{X}$
6 1 1 txuni ${⊢}\left({J}\in \mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to {X}×{X}=\bigcup \left({J}{×}_{t}{J}\right)$
7 6 anidms ${⊢}{J}\in \mathrm{Top}\to {X}×{X}=\bigcup \left({J}{×}_{t}{J}\right)$
8 5 7 sseqtrid ${⊢}{J}\in \mathrm{Top}\to {\mathrm{I}↾}_{{X}}\subseteq \bigcup \left({J}{×}_{t}{J}\right)$
9 eqid ${⊢}\bigcup \left({J}{×}_{t}{J}\right)=\bigcup \left({J}{×}_{t}{J}\right)$
10 9 iscld2 ${⊢}\left({J}{×}_{t}{J}\in \mathrm{Top}\wedge {\mathrm{I}↾}_{{X}}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\right)\to \left({\mathrm{I}↾}_{{X}}\in \mathrm{Clsd}\left({J}{×}_{t}{J}\right)↔\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\in \left({J}{×}_{t}{J}\right)\right)$
11 4 8 10 syl2anc ${⊢}{J}\in \mathrm{Top}\to \left({\mathrm{I}↾}_{{X}}\in \mathrm{Clsd}\left({J}{×}_{t}{J}\right)↔\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\in \left({J}{×}_{t}{J}\right)\right)$
12 eltx ${⊢}\left({J}\in \mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\in \left({J}{×}_{t}{J}\right)↔\forall {e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
13 12 anidms ${⊢}{J}\in \mathrm{Top}\to \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\in \left({J}{×}_{t}{J}\right)↔\forall {e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
14 eldif ${⊢}{e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left({e}\in \bigcup \left({J}{×}_{t}{J}\right)\wedge ¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\right)$
15 7 eqcomd ${⊢}{J}\in \mathrm{Top}\to \bigcup \left({J}{×}_{t}{J}\right)={X}×{X}$
16 15 eleq2d ${⊢}{J}\in \mathrm{Top}\to \left({e}\in \bigcup \left({J}{×}_{t}{J}\right)↔{e}\in \left({X}×{X}\right)\right)$
17 16 anbi1d ${⊢}{J}\in \mathrm{Top}\to \left(\left({e}\in \bigcup \left({J}{×}_{t}{J}\right)\wedge ¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left({e}\in \left({X}×{X}\right)\wedge ¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
18 14 17 syl5bb ${⊢}{J}\in \mathrm{Top}\to \left({e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left({e}\in \left({X}×{X}\right)\wedge ¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
19 18 imbi1d ${⊢}{J}\in \mathrm{Top}\to \left(\left({e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\left(\left({e}\in \left({X}×{X}\right)\wedge ¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)\right)$
20 impexp ${⊢}\left(\left({e}\in \left({X}×{X}\right)\wedge ¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\left({e}\in \left({X}×{X}\right)\to \left(¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)\right)$
21 19 20 syl6bb ${⊢}{J}\in \mathrm{Top}\to \left(\left({e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\left({e}\in \left({X}×{X}\right)\to \left(¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)\right)\right)$
22 21 ralbidv2 ${⊢}{J}\in \mathrm{Top}\to \left(\forall {e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\forall {e}\in \left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left(¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)\right)$
23 eleq1 ${⊢}{e}=⟨{a},{b}⟩\to \left({e}\in \left({\mathrm{I}↾}_{{X}}\right)↔⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\right)$
24 23 notbid ${⊢}{e}=⟨{a},{b}⟩\to \left(¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)↔¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\right)$
25 eleq1 ${⊢}{e}=⟨{a},{b}⟩\to \left({e}\in \left({c}×{d}\right)↔⟨{a},{b}⟩\in \left({c}×{d}\right)\right)$
26 25 anbi1d ${⊢}{e}=⟨{a},{b}⟩\to \left(\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
27 26 2rexbidv ${⊢}{e}=⟨{a},{b}⟩\to \left(\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
28 24 27 imbi12d ${⊢}{e}=⟨{a},{b}⟩\to \left(\left(¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\left(¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)\right)$
29 28 ralxp ${⊢}\forall {e}\in \left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left(¬{e}\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)$
30 22 29 syl6bb ${⊢}{J}\in \mathrm{Top}\to \left(\forall {e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)\right)$
31 vex ${⊢}{b}\in \mathrm{V}$
32 31 opelresi ${⊢}⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)↔\left({a}\in {X}\wedge ⟨{a},{b}⟩\in \mathrm{I}\right)$
33 df-br ${⊢}{a}\mathrm{I}{b}↔⟨{a},{b}⟩\in \mathrm{I}$
34 31 ideq ${⊢}{a}\mathrm{I}{b}↔{a}={b}$
35 33 34 bitr3i ${⊢}⟨{a},{b}⟩\in \mathrm{I}↔{a}={b}$
36 ibar ${⊢}{a}\in {X}\to \left(⟨{a},{b}⟩\in \mathrm{I}↔\left({a}\in {X}\wedge ⟨{a},{b}⟩\in \mathrm{I}\right)\right)$
37 36 adantr ${⊢}\left({a}\in {X}\wedge {b}\in {X}\right)\to \left(⟨{a},{b}⟩\in \mathrm{I}↔\left({a}\in {X}\wedge ⟨{a},{b}⟩\in \mathrm{I}\right)\right)$
38 35 37 syl5rbbr ${⊢}\left({a}\in {X}\wedge {b}\in {X}\right)\to \left(\left({a}\in {X}\wedge ⟨{a},{b}⟩\in \mathrm{I}\right)↔{a}={b}\right)$
39 32 38 syl5bb ${⊢}\left({a}\in {X}\wedge {b}\in {X}\right)\to \left(⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)↔{a}={b}\right)$
40 39 adantl ${⊢}\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\to \left(⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)↔{a}={b}\right)$
41 40 necon3bbid ${⊢}\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\to \left(¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)↔{a}\ne {b}\right)$
42 elssuni ${⊢}{c}\in {J}\to {c}\subseteq \bigcup {J}$
43 elssuni ${⊢}{d}\in {J}\to {d}\subseteq \bigcup {J}$
44 xpss12 ${⊢}\left({c}\subseteq \bigcup {J}\wedge {d}\subseteq \bigcup {J}\right)\to {c}×{d}\subseteq \bigcup {J}×\bigcup {J}$
45 42 43 44 syl2an ${⊢}\left({c}\in {J}\wedge {d}\in {J}\right)\to {c}×{d}\subseteq \bigcup {J}×\bigcup {J}$
46 1 1 xpeq12i ${⊢}{X}×{X}=\bigcup {J}×\bigcup {J}$
47 45 46 sseqtrrdi ${⊢}\left({c}\in {J}\wedge {d}\in {J}\right)\to {c}×{d}\subseteq {X}×{X}$
48 47 adantl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to {c}×{d}\subseteq {X}×{X}$
49 7 ad2antrr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to {X}×{X}=\bigcup \left({J}{×}_{t}{J}\right)$
50 48 49 sseqtrd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)$
51 reldisj ${⊢}{c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\to \left(\left({c}×{d}\right)\cap \left({\mathrm{I}↾}_{{X}}\right)=\varnothing ↔{c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)$
52 50 51 syl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left(\left({c}×{d}\right)\cap \left({\mathrm{I}↾}_{{X}}\right)=\varnothing ↔{c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)$
53 df-res ${⊢}{\mathrm{I}↾}_{{X}}=\mathrm{I}\cap \left({X}×\mathrm{V}\right)$
54 53 ineq2i ${⊢}\left({c}×{d}\right)\cap \left({\mathrm{I}↾}_{{X}}\right)=\left({c}×{d}\right)\cap \left(\mathrm{I}\cap \left({X}×\mathrm{V}\right)\right)$
55 inass ${⊢}\left(\left({c}×{d}\right)\cap \mathrm{I}\right)\cap \left({X}×\mathrm{V}\right)=\left({c}×{d}\right)\cap \left(\mathrm{I}\cap \left({X}×\mathrm{V}\right)\right)$
56 inss1 ${⊢}\left({c}×{d}\right)\cap \mathrm{I}\subseteq {c}×{d}$
57 56 48 sstrid ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left({c}×{d}\right)\cap \mathrm{I}\subseteq {X}×{X}$
58 ssv ${⊢}{X}\subseteq \mathrm{V}$
59 xpss2 ${⊢}{X}\subseteq \mathrm{V}\to {X}×{X}\subseteq {X}×\mathrm{V}$
60 58 59 ax-mp ${⊢}{X}×{X}\subseteq {X}×\mathrm{V}$
61 57 60 sstrdi ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left({c}×{d}\right)\cap \mathrm{I}\subseteq {X}×\mathrm{V}$
62 df-ss ${⊢}\left({c}×{d}\right)\cap \mathrm{I}\subseteq {X}×\mathrm{V}↔\left(\left({c}×{d}\right)\cap \mathrm{I}\right)\cap \left({X}×\mathrm{V}\right)=\left({c}×{d}\right)\cap \mathrm{I}$
63 61 62 sylib ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left(\left({c}×{d}\right)\cap \mathrm{I}\right)\cap \left({X}×\mathrm{V}\right)=\left({c}×{d}\right)\cap \mathrm{I}$
64 55 63 syl5eqr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left({c}×{d}\right)\cap \left(\mathrm{I}\cap \left({X}×\mathrm{V}\right)\right)=\left({c}×{d}\right)\cap \mathrm{I}$
65 54 64 syl5eq ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left({c}×{d}\right)\cap \left({\mathrm{I}↾}_{{X}}\right)=\left({c}×{d}\right)\cap \mathrm{I}$
66 65 eqeq1d ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left(\left({c}×{d}\right)\cap \left({\mathrm{I}↾}_{{X}}\right)=\varnothing ↔\left({c}×{d}\right)\cap \mathrm{I}=\varnothing \right)$
67 opelxp ${⊢}⟨{a},{a}⟩\in \left({c}×{d}\right)↔\left({a}\in {c}\wedge {a}\in {d}\right)$
68 df-br ${⊢}{a}\left({c}×{d}\right){a}↔⟨{a},{a}⟩\in \left({c}×{d}\right)$
69 elin ${⊢}{a}\in \left({c}\cap {d}\right)↔\left({a}\in {c}\wedge {a}\in {d}\right)$
70 67 68 69 3bitr4i ${⊢}{a}\left({c}×{d}\right){a}↔{a}\in \left({c}\cap {d}\right)$
71 70 notbii ${⊢}¬{a}\left({c}×{d}\right){a}↔¬{a}\in \left({c}\cap {d}\right)$
72 71 albii ${⊢}\forall {a}\phantom{\rule{.4em}{0ex}}¬{a}\left({c}×{d}\right){a}↔\forall {a}\phantom{\rule{.4em}{0ex}}¬{a}\in \left({c}\cap {d}\right)$
73 intirr ${⊢}\left({c}×{d}\right)\cap \mathrm{I}=\varnothing ↔\forall {a}\phantom{\rule{.4em}{0ex}}¬{a}\left({c}×{d}\right){a}$
74 eq0 ${⊢}{c}\cap {d}=\varnothing ↔\forall {a}\phantom{\rule{.4em}{0ex}}¬{a}\in \left({c}\cap {d}\right)$
75 72 73 74 3bitr4i ${⊢}\left({c}×{d}\right)\cap \mathrm{I}=\varnothing ↔{c}\cap {d}=\varnothing$
76 66 75 syl6bb ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left(\left({c}×{d}\right)\cap \left({\mathrm{I}↾}_{{X}}\right)=\varnothing ↔{c}\cap {d}=\varnothing \right)$
77 52 76 bitr3d ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left({c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)↔{c}\cap {d}=\varnothing \right)$
78 77 anbi2d ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left(\left(\left({a}\in {c}\wedge {b}\in {d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left(\left({a}\in {c}\wedge {b}\in {d}\right)\wedge {c}\cap {d}=\varnothing \right)\right)$
79 opelxp ${⊢}⟨{a},{b}⟩\in \left({c}×{d}\right)↔\left({a}\in {c}\wedge {b}\in {d}\right)$
80 79 anbi1i ${⊢}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left(\left({a}\in {c}\wedge {b}\in {d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)$
81 df-3an ${⊢}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)↔\left(\left({a}\in {c}\wedge {b}\in {d}\right)\wedge {c}\cap {d}=\varnothing \right)$
82 78 80 81 3bitr4g ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\wedge \left({c}\in {J}\wedge {d}\in {J}\right)\right)\to \left(\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)$
83 82 2rexbidva ${⊢}\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\to \left(\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)$
84 41 83 imbi12d ${⊢}\left({J}\in \mathrm{Top}\wedge \left({a}\in {X}\wedge {b}\in {X}\right)\right)\to \left(\left(¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\left({a}\ne {b}\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)\right)$
85 84 2ralbidva ${⊢}{J}\in \mathrm{Top}\to \left(\forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬⟨{a},{b}⟩\in \left({\mathrm{I}↾}_{{X}}\right)\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left(⟨{a},{b}⟩\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\right)↔\forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)\right)$
86 30 85 bitrd ${⊢}{J}\in \mathrm{Top}\to \left(\forall {e}\in \left(\bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({e}\in \left({c}×{d}\right)\wedge {c}×{d}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\setminus \left({\mathrm{I}↾}_{{X}}\right)\right)↔\forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)\right)$
87 11 13 86 3bitrrd ${⊢}{J}\in \mathrm{Top}\to \left(\forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)↔{\mathrm{I}↾}_{{X}}\in \mathrm{Clsd}\left({J}{×}_{t}{J}\right)\right)$
88 87 pm5.32i ${⊢}\left({J}\in \mathrm{Top}\wedge \forall {a}\in {X}\phantom{\rule{.4em}{0ex}}\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists {c}\in {J}\phantom{\rule{.4em}{0ex}}\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}\left({a}\in {c}\wedge {b}\in {d}\wedge {c}\cap {d}=\varnothing \right)\right)\right)↔\left({J}\in \mathrm{Top}\wedge {\mathrm{I}↾}_{{X}}\in \mathrm{Clsd}\left({J}{×}_{t}{J}\right)\right)$
89 2 88 bitri ${⊢}{J}\in \mathrm{Haus}↔\left({J}\in \mathrm{Top}\wedge {\mathrm{I}↾}_{{X}}\in \mathrm{Clsd}\left({J}{×}_{t}{J}\right)\right)$