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 df-br a I b a b I
34 31 ideq a I b a = b
35 33 34 bitr3i a b I a = b
36 ibar a X a b I a X a b I
37 36 adantr a X b X a b I a X a b I
38 35 37 syl5rbbr 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