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=⋃J
Assertion hausdiag ⊢J∈Haus↔J∈Top∧I↾X∈Clsd⁡J×tJ

Proof

Step Hyp Ref Expression
1 hausdiag.x ⊢X=⋃J
2 1 ishaus ⊢J∈Haus↔J∈Top∧∀a∈X∀b∈Xa≠b→∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅
3 txtop ⊢J∈Top∧J∈Top→J×tJ∈Top
4 3 anidms ⊢J∈Top→J×tJ∈Top
5 idssxp ⊢I↾X⊆X×X
6 1 1 txuni ⊢J∈Top∧J∈Top→X×X=⋃J×tJ
7 6 anidms ⊢J∈Top→X×X=⋃J×tJ
8 5 7 sseqtrid ⊢J∈Top→I↾X⊆⋃J×tJ
9 eqid ⊢⋃J×tJ=⋃J×tJ
10 9 iscld2 ⊢J×tJ∈Top∧I↾X⊆⋃J×tJ→I↾X∈Clsd⁡J×tJ↔⋃J×tJ∖I↾X∈J×tJ
11 4 8 10 syl2anc ⊢J∈Top→I↾X∈Clsd⁡J×tJ↔⋃J×tJ∖I↾X∈J×tJ
12 eltx ⊢J∈Top∧J∈Top→⋃J×tJ∖I↾X∈J×tJ↔∀e∈⋃J×tJ∖I↾X∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X
13 12 anidms ⊢J∈Top→⋃J×tJ∖I↾X∈J×tJ↔∀e∈⋃J×tJ∖I↾X∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X
14 eldif ⊢e∈⋃J×tJ∖I↾X↔e∈⋃J×tJ∧¬e∈I↾X
15 7 eqcomd ⊢J∈Top→⋃J×tJ=X×X
16 15 eleq2d ⊢J∈Top→e∈⋃J×tJ↔e∈X×X
17 16 anbi1d ⊢J∈Top→e∈⋃J×tJ∧¬e∈I↾X↔e∈X×X∧¬e∈I↾X
18 14 17 bitrid ⊢J∈Top→e∈⋃J×tJ∖I↾X↔e∈X×X∧¬e∈I↾X
19 18 imbi1d ⊢J∈Top→e∈⋃J×tJ∖I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔e∈X×X∧¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X
20 impexp ⊢e∈X×X∧¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔e∈X×X→¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X
21 19 20 bitrdi ⊢J∈Top→e∈⋃J×tJ∖I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔e∈X×X→¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X
22 21 ralbidv2 ⊢J∈Top→∀e∈⋃J×tJ∖I↾X∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∀e∈X×X¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X
23 eleq1 ⊢e=ab→e∈I↾X↔ab∈I↾X
24 23 notbid ⊢e=ab→¬e∈I↾X↔¬ab∈I↾X
25 eleq1 ⊢e=ab→e∈c×d↔ab∈c×d
26 25 anbi1d ⊢e=ab→e∈c×d∧c×d⊆⋃J×tJ∖I↾X↔ab∈c×d∧c×d⊆⋃J×tJ∖I↾X
27 26 2rexbidv ⊢e=ab→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X
28 24 27 imbi12d ⊢e=ab→¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔¬ab∈I↾X→∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X
29 28 ralxp ⊢∀e∈X×X¬e∈I↾X→∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∀a∈X∀b∈X¬ab∈I↾X→∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X
30 22 29 bitrdi ⊢J∈Top→∀e∈⋃J×tJ∖I↾X∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∀a∈X∀b∈X¬ab∈I↾X→∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X
31 vex ⊢b∈V
32 31 opelresi ⊢ab∈I↾X↔a∈X∧ab∈I
33 ibar ⊢a∈X→ab∈I↔a∈X∧ab∈I
34 33 adantr ⊢a∈X∧b∈X→ab∈I↔a∈X∧ab∈I
35 df-br ⊢aIb↔ab∈I
36 31 ideq ⊢aIb↔a=b
37 35 36 bitr3i ⊢ab∈I↔a=b
38 34 37 bitr3di ⊢a∈X∧b∈X→a∈X∧ab∈I↔a=b
39 32 38 bitrid ⊢a∈X∧b∈X→ab∈I↾X↔a=b
40 39 adantl ⊢J∈Top∧a∈X∧b∈X→ab∈I↾X↔a=b
41 40 necon3bbid ⊢J∈Top∧a∈X∧b∈X→¬ab∈I↾X↔a≠b
42 elssuni ⊢c∈J→c⊆⋃J
43 elssuni ⊢d∈J→d⊆⋃J
44 xpss12 ⊢c⊆⋃J∧d⊆⋃J→c×d⊆⋃J×⋃J
45 42 43 44 syl2an ⊢c∈J∧d∈J→c×d⊆⋃J×⋃J
46 1 1 xpeq12i ⊢X×X=⋃J×⋃J
47 45 46 sseqtrrdi ⊢c∈J∧d∈J→c×d⊆X×X
48 47 adantl ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d⊆X×X
49 7 ad2antrr ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→X×X=⋃J×tJ
50 48 49 sseqtrd ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d⊆⋃J×tJ
51 reldisj ⊢c×d⊆⋃J×tJ→c×d∩I↾X=∅↔c×d⊆⋃J×tJ∖I↾X
52 50 51 syl ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I↾X=∅↔c×d⊆⋃J×tJ∖I↾X
53 df-res ⊢I↾X=I∩X×V
54 53 ineq2i ⊢c×d∩I↾X=c×d∩I∩X×V
55 inass ⊢c×d∩I∩X×V=c×d∩I∩X×V
56 inss1 ⊢c×d∩I⊆c×d
57 56 48 sstrid ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I⊆X×X
58 ssv ⊢X⊆V
59 xpss2 ⊢X⊆V→X×X⊆X×V
60 58 59 ax-mp ⊢X×X⊆X×V
61 57 60 sstrdi ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I⊆X×V
62 df-ss ⊢c×d∩I⊆X×V↔c×d∩I∩X×V=c×d∩I
63 61 62 sylib ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I∩X×V=c×d∩I
64 55 63 eqtr3id ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I∩X×V=c×d∩I
65 54 64 eqtrid ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I↾X=c×d∩I
66 65 eqeq1d ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I↾X=∅↔c×d∩I=∅
67 opelxp ⊢aa∈c×d↔a∈c∧a∈d
68 df-br ⊢ac×da↔aa∈c×d
69 elin ⊢a∈c∩d↔a∈c∧a∈d
70 67 68 69 3bitr4i ⊢ac×da↔a∈c∩d
71 70 notbii ⊢¬ac×da↔¬a∈c∩d
72 71 albii ⊢∀a¬ac×da↔∀a¬a∈c∩d
73 intirr ⊢c×d∩I=∅↔∀a¬ac×da
74 eq0 ⊢c∩d=∅↔∀a¬a∈c∩d
75 72 73 74 3bitr4i ⊢c×d∩I=∅↔c∩d=∅
76 66 75 bitrdi ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d∩I↾X=∅↔c∩d=∅
77 52 76 bitr3d ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→c×d⊆⋃J×tJ∖I↾X↔c∩d=∅
78 77 anbi2d ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→a∈c∧b∈d∧c×d⊆⋃J×tJ∖I↾X↔a∈c∧b∈d∧c∩d=∅
79 opelxp ⊢ab∈c×d↔a∈c∧b∈d
80 79 anbi1i ⊢ab∈c×d∧c×d⊆⋃J×tJ∖I↾X↔a∈c∧b∈d∧c×d⊆⋃J×tJ∖I↾X
81 df-3an ⊢a∈c∧b∈d∧c∩d=∅↔a∈c∧b∈d∧c∩d=∅
82 78 80 81 3bitr4g ⊢J∈Top∧a∈X∧b∈X∧c∈J∧d∈J→ab∈c×d∧c×d⊆⋃J×tJ∖I↾X↔a∈c∧b∈d∧c∩d=∅
83 82 2rexbidva ⊢J∈Top∧a∈X∧b∈X→∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅
84 41 83 imbi12d ⊢J∈Top∧a∈X∧b∈X→¬ab∈I↾X→∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X↔a≠b→∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅
85 84 2ralbidva ⊢J∈Top→∀a∈X∀b∈X¬ab∈I↾X→∃c∈J∃d∈Jab∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∀a∈X∀b∈Xa≠b→∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅
86 30 85 bitrd ⊢J∈Top→∀e∈⋃J×tJ∖I↾X∃c∈J∃d∈Je∈c×d∧c×d⊆⋃J×tJ∖I↾X↔∀a∈X∀b∈Xa≠b→∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅
87 11 13 86 3bitrrd ⊢J∈Top→∀a∈X∀b∈Xa≠b→∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅↔I↾X∈Clsd⁡J×tJ
88 87 pm5.32i ⊢J∈Top∧∀a∈X∀b∈Xa≠b→∃c∈J∃d∈Ja∈c∧b∈d∧c∩d=∅↔J∈Top∧I↾X∈Clsd⁡J×tJ
89 2 88 bitri ⊢J∈Haus↔J∈Top∧I↾X∈Clsd⁡J×tJ