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 × t J

Proof

Step Hyp Ref Expression
1 hausdiag.x ⊢ X = ⋃ J
2 1 ishaus ⊢ J ∈ Haus ↔ J ∈ Top ∧ ∀ a ∈ X ∀ b ∈ X a ≠ b → ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
3 txtop ⊢ J ∈ Top ∧ J ∈ Top → J × t J ∈ Top
4 3 anidms ⊢ J ∈ Top → J × t J ∈ Top
5 idssxp ⊢ I ↾ X ⊆ X × X
6 1 1 txuni ⊢ J ∈ Top ∧ J ∈ Top → X × X = ⋃ J × t J
7 6 anidms ⊢ J ∈ Top → X × X = ⋃ J × t J
8 5 7 sseqtrid ⊢ J ∈ Top → I ↾ X ⊆ ⋃ J × t J
9 eqid ⊢ ⋃ J × t J = ⋃ J × t J
10 9 iscld2 ⊢ J × t J ∈ Top ∧ I ↾ X ⊆ ⋃ J × t J → I ↾ X ∈ Clsd ⁡ J × t J ↔ ⋃ J × t J ∖ I ↾ X ∈ J × t J
11 4 8 10 syl2anc ⊢ J ∈ Top → I ↾ X ∈ Clsd ⁡ J × t J ↔ ⋃ J × t J ∖ I ↾ X ∈ J × t J
12 eltx ⊢ J ∈ Top ∧ J ∈ Top → ⋃ J × t J ∖ I ↾ X ∈ J × t J ↔ ∀ e ∈ ⋃ J × t J ∖ I ↾ X ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
13 12 anidms ⊢ J ∈ Top → ⋃ J × t J ∖ I ↾ X ∈ J × t J ↔ ∀ e ∈ ⋃ J × t J ∖ I ↾ X ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
14 eldif ⊢ e ∈ ⋃ J × t J ∖ I ↾ X ↔ e ∈ ⋃ J × t J ∧ ¬ e ∈ I ↾ X
15 7 eqcomd ⊢ J ∈ Top → ⋃ J × t J = X × X
16 15 eleq2d ⊢ J ∈ Top → e ∈ ⋃ J × t J ↔ e ∈ X × X
17 16 anbi1d ⊢ J ∈ Top → e ∈ ⋃ J × t J ∧ ¬ e ∈ I ↾ X ↔ e ∈ X × X ∧ ¬ e ∈ I ↾ X
18 14 17 syl5bb ⊢ J ∈ Top → e ∈ ⋃ J × t J ∖ I ↾ X ↔ e ∈ X × X ∧ ¬ e ∈ I ↾ X
19 18 imbi1d ⊢ J ∈ Top → e ∈ ⋃ J × t J ∖ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ e ∈ X × X ∧ ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
20 impexp ⊢ e ∈ X × X ∧ ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ e ∈ X × X → ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
21 19 20 syl6bb ⊢ J ∈ Top → e ∈ ⋃ J × t J ∖ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ e ∈ X × X → ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
22 21 ralbidv2 ⊢ J ∈ Top → ∀ e ∈ ⋃ J × t J ∖ I ↾ X ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∀ e ∈ X × X ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
23 eleq1 ⊢ e = a b → e ∈ I ↾ X ↔ a b ∈ I ↾ X
24 23 notbid ⊢ e = a b → ¬ e ∈ I ↾ X ↔ ¬ a b ∈ I ↾ X
25 eleq1 ⊢ e = a b → e ∈ c × d ↔ a b ∈ c × d
26 25 anbi1d ⊢ e = a b → e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
27 26 2rexbidv ⊢ e = a b → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
28 24 27 imbi12d ⊢ e = a b → ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ¬ a b ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
29 28 ralxp ⊢ ∀ e ∈ X × X ¬ e ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∀ a ∈ X ∀ b ∈ X ¬ a b ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
30 22 29 syl6bb ⊢ J ∈ Top → ∀ e ∈ ⋃ J × t J ∖ I ↾ X ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∀ a ∈ X ∀ b ∈ X ¬ a b ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X
31 vex ⊢ b ∈ V
32 31 opelresi ⊢ a b ∈ I ↾ X ↔ a ∈ X ∧ a b ∈ I
33 ibar ⊢ a ∈ X → a b ∈ I ↔ a ∈ X ∧ a b ∈ I
34 33 adantr ⊢ a ∈ X ∧ b ∈ X → a b ∈ I ↔ a ∈ X ∧ a b ∈ I
35 df-br ⊢ a I b ↔ a b ∈ I
36 31 ideq ⊢ a I b ↔ a = b
37 35 36 bitr3i ⊢ a b ∈ I ↔ a = b
38 34 37 bitr3di ⊢ a ∈ X ∧ b ∈ X → a ∈ X ∧ a b ∈ I ↔ a = b
39 32 38 syl5bb ⊢ a ∈ X ∧ b ∈ X → a b ∈ I ↾ X ↔ a = b
40 39 adantl ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X → a b ∈ I ↾ X ↔ a = b
41 40 necon3bbid ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X → ¬ a b ∈ 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 × t J
50 48 49 sseqtrd ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X ∧ c ∈ J ∧ d ∈ J → c × d ⊆ ⋃ J × t J
51 reldisj ⊢ c × d ⊆ ⋃ J × t J → c × d ∩ I ↾ X = ∅ ↔ c × d ⊆ ⋃ J × t J ∖ I ↾ X
52 50 51 syl ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X ∧ c ∈ J ∧ d ∈ J → c × d ∩ I ↾ X = ∅ ↔ c × d ⊆ ⋃ J × t J ∖ 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 syl5eqr ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X ∧ c ∈ J ∧ d ∈ J → c × d ∩ I ∩ X × V = c × d ∩ I
65 54 64 syl5eq ⊢ 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 ⊢ a a ∈ c × d ↔ a ∈ c ∧ a ∈ d
68 df-br ⊢ a c × d a ↔ a a ∈ c × d
69 elin ⊢ a ∈ c ∩ d ↔ a ∈ c ∧ a ∈ d
70 67 68 69 3bitr4i ⊢ a c × d a ↔ a ∈ c ∩ d
71 70 notbii ⊢ ¬ a c × d a ↔ ¬ a ∈ c ∩ d
72 71 albii ⊢ ∀ a ¬ a c × d a ↔ ∀ a ¬ a ∈ c ∩ d
73 intirr ⊢ c × d ∩ I = ∅ ↔ ∀ a ¬ a c × d a
74 eq0 ⊢ c ∩ d = ∅ ↔ ∀ a ¬ a ∈ c ∩ d
75 72 73 74 3bitr4i ⊢ c × d ∩ I = ∅ ↔ c ∩ d = ∅
76 66 75 syl6bb ⊢ 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 × t J ∖ I ↾ X ↔ c ∩ d = ∅
78 77 anbi2d ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X ∧ c ∈ J ∧ d ∈ J → a ∈ c ∧ b ∈ d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
79 opelxp ⊢ a b ∈ c × d ↔ a ∈ c ∧ b ∈ d
80 79 anbi1i ⊢ a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ a ∈ c ∧ b ∈ d ∧ c × d ⊆ ⋃ J × t J ∖ 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 → a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
83 82 2rexbidva ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X → ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
84 41 83 imbi12d ⊢ J ∈ Top ∧ a ∈ X ∧ b ∈ X → ¬ a b ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ a ≠ b → ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
85 84 2ralbidva ⊢ J ∈ Top → ∀ a ∈ X ∀ b ∈ X ¬ a b ∈ I ↾ X → ∃ c ∈ J ∃ d ∈ J a b ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∀ a ∈ X ∀ b ∈ X a ≠ b → ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
86 30 85 bitrd ⊢ J ∈ Top → ∀ e ∈ ⋃ J × t J ∖ I ↾ X ∃ c ∈ J ∃ d ∈ J e ∈ c × d ∧ c × d ⊆ ⋃ J × t J ∖ I ↾ X ↔ ∀ a ∈ X ∀ b ∈ X a ≠ b → ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅
87 11 13 86 3bitrrd ⊢ J ∈ Top → ∀ a ∈ X ∀ b ∈ X a ≠ b → ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅ ↔ I ↾ X ∈ Clsd ⁡ J × t J
88 87 pm5.32i ⊢ J ∈ Top ∧ ∀ a ∈ X ∀ b ∈ X a ≠ b → ∃ c ∈ J ∃ d ∈ J a ∈ c ∧ b ∈ d ∧ c ∩ d = ∅ ↔ J ∈ Top ∧ I ↾ X ∈ Clsd ⁡ J × t J
89 2 88 bitri ⊢ J ∈ Haus ↔ J ∈ Top ∧ I ↾ X ∈ Clsd ⁡ J × t J