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 = U. J
Assertion hausdiag
|- ( J e. Haus <-> ( J e. Top /\ ( _I |` X ) e. ( Clsd ` ( J tX J ) ) ) )

Proof

Step Hyp Ref Expression
1 hausdiag.x
 |-  X = U. J
2 1 ishaus
 |-  ( J e. Haus <-> ( J e. Top /\ A. a e. X A. b e. X ( a =/= b -> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) ) )
3 txtop
 |-  ( ( J e. Top /\ J e. Top ) -> ( J tX J ) e. Top )
4 3 anidms
 |-  ( J e. Top -> ( J tX J ) e. Top )
5 idssxp
 |-  ( _I |` X ) C_ ( X X. X )
6 1 1 txuni
 |-  ( ( J e. Top /\ J e. Top ) -> ( X X. X ) = U. ( J tX J ) )
7 6 anidms
 |-  ( J e. Top -> ( X X. X ) = U. ( J tX J ) )
8 5 7 sseqtrid
 |-  ( J e. Top -> ( _I |` X ) C_ U. ( J tX J ) )
9 eqid
 |-  U. ( J tX J ) = U. ( J tX J )
10 9 iscld2
 |-  ( ( ( J tX J ) e. Top /\ ( _I |` X ) C_ U. ( J tX J ) ) -> ( ( _I |` X ) e. ( Clsd ` ( J tX J ) ) <-> ( U. ( J tX J ) \ ( _I |` X ) ) e. ( J tX J ) ) )
11 4 8 10 syl2anc
 |-  ( J e. Top -> ( ( _I |` X ) e. ( Clsd ` ( J tX J ) ) <-> ( U. ( J tX J ) \ ( _I |` X ) ) e. ( J tX J ) ) )
12 eltx
 |-  ( ( J e. Top /\ J e. Top ) -> ( ( U. ( J tX J ) \ ( _I |` X ) ) e. ( J tX J ) <-> A. e e. ( U. ( J tX J ) \ ( _I |` X ) ) E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) )
13 12 anidms
 |-  ( J e. Top -> ( ( U. ( J tX J ) \ ( _I |` X ) ) e. ( J tX J ) <-> A. e e. ( U. ( J tX J ) \ ( _I |` X ) ) E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) )
14 eldif
 |-  ( e e. ( U. ( J tX J ) \ ( _I |` X ) ) <-> ( e e. U. ( J tX J ) /\ -. e e. ( _I |` X ) ) )
15 7 eqcomd
 |-  ( J e. Top -> U. ( J tX J ) = ( X X. X ) )
16 15 eleq2d
 |-  ( J e. Top -> ( e e. U. ( J tX J ) <-> e e. ( X X. X ) ) )
17 16 anbi1d
 |-  ( J e. Top -> ( ( e e. U. ( J tX J ) /\ -. e e. ( _I |` X ) ) <-> ( e e. ( X X. X ) /\ -. e e. ( _I |` X ) ) ) )
18 14 17 syl5bb
 |-  ( J e. Top -> ( e e. ( U. ( J tX J ) \ ( _I |` X ) ) <-> ( e e. ( X X. X ) /\ -. e e. ( _I |` X ) ) ) )
19 18 imbi1d
 |-  ( J e. Top -> ( ( e e. ( U. ( J tX J ) \ ( _I |` X ) ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> ( ( e e. ( X X. X ) /\ -. e e. ( _I |` X ) ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) ) )
20 impexp
 |-  ( ( ( e e. ( X X. X ) /\ -. e e. ( _I |` X ) ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> ( e e. ( X X. X ) -> ( -. e e. ( _I |` X ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) ) )
21 19 20 bitrdi
 |-  ( J e. Top -> ( ( e e. ( U. ( J tX J ) \ ( _I |` X ) ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> ( e e. ( X X. X ) -> ( -. e e. ( _I |` X ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) ) ) )
22 21 ralbidv2
 |-  ( J e. Top -> ( A. e e. ( U. ( J tX J ) \ ( _I |` X ) ) E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> A. e e. ( X X. X ) ( -. e e. ( _I |` X ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) ) )
23 eleq1
 |-  ( e = <. a , b >. -> ( e e. ( _I |` X ) <-> <. a , b >. e. ( _I |` X ) ) )
24 23 notbid
 |-  ( e = <. a , b >. -> ( -. e e. ( _I |` X ) <-> -. <. a , b >. e. ( _I |` X ) ) )
25 eleq1
 |-  ( e = <. a , b >. -> ( e e. ( c X. d ) <-> <. a , b >. e. ( c X. d ) ) )
26 25 anbi1d
 |-  ( e = <. a , b >. -> ( ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) )
27 26 2rexbidv
 |-  ( e = <. a , b >. -> ( E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) )
28 24 27 imbi12d
 |-  ( e = <. a , b >. -> ( ( -. e e. ( _I |` X ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> ( -. <. a , b >. e. ( _I |` X ) -> E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) ) )
29 28 ralxp
 |-  ( A. e e. ( X X. X ) ( -. e e. ( _I |` X ) -> E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> A. a e. X A. b e. X ( -. <. a , b >. e. ( _I |` X ) -> E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) )
30 22 29 bitrdi
 |-  ( J e. Top -> ( A. e e. ( U. ( J tX J ) \ ( _I |` X ) ) E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> A. a e. X A. b e. X ( -. <. a , b >. e. ( _I |` X ) -> E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) ) )
31 vex
 |-  b e. _V
32 31 opelresi
 |-  ( <. a , b >. e. ( _I |` X ) <-> ( a e. X /\ <. a , b >. e. _I ) )
33 ibar
 |-  ( a e. X -> ( <. a , b >. e. _I <-> ( a e. X /\ <. a , b >. e. _I ) ) )
34 33 adantr
 |-  ( ( a e. X /\ b e. X ) -> ( <. a , b >. e. _I <-> ( a e. X /\ <. a , b >. e. _I ) ) )
35 df-br
 |-  ( a _I b <-> <. a , b >. e. _I )
36 31 ideq
 |-  ( a _I b <-> a = b )
37 35 36 bitr3i
 |-  ( <. a , b >. e. _I <-> a = b )
38 34 37 bitr3di
 |-  ( ( a e. X /\ b e. X ) -> ( ( a e. X /\ <. a , b >. e. _I ) <-> a = b ) )
39 32 38 syl5bb
 |-  ( ( a e. X /\ b e. X ) -> ( <. a , b >. e. ( _I |` X ) <-> a = b ) )
40 39 adantl
 |-  ( ( J e. Top /\ ( a e. X /\ b e. X ) ) -> ( <. a , b >. e. ( _I |` X ) <-> a = b ) )
41 40 necon3bbid
 |-  ( ( J e. Top /\ ( a e. X /\ b e. X ) ) -> ( -. <. a , b >. e. ( _I |` X ) <-> a =/= b ) )
42 elssuni
 |-  ( c e. J -> c C_ U. J )
43 elssuni
 |-  ( d e. J -> d C_ U. J )
44 xpss12
 |-  ( ( c C_ U. J /\ d C_ U. J ) -> ( c X. d ) C_ ( U. J X. U. J ) )
45 42 43 44 syl2an
 |-  ( ( c e. J /\ d e. J ) -> ( c X. d ) C_ ( U. J X. U. J ) )
46 1 1 xpeq12i
 |-  ( X X. X ) = ( U. J X. U. J )
47 45 46 sseqtrrdi
 |-  ( ( c e. J /\ d e. J ) -> ( c X. d ) C_ ( X X. X ) )
48 47 adantl
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( c X. d ) C_ ( X X. X ) )
49 7 ad2antrr
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( X X. X ) = U. ( J tX J ) )
50 48 49 sseqtrd
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( c X. d ) C_ U. ( J tX J ) )
51 reldisj
 |-  ( ( c X. d ) C_ U. ( J tX J ) -> ( ( ( c X. d ) i^i ( _I |` X ) ) = (/) <-> ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) )
52 50 51 syl
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( c X. d ) i^i ( _I |` X ) ) = (/) <-> ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) )
53 df-res
 |-  ( _I |` X ) = ( _I i^i ( X X. _V ) )
54 53 ineq2i
 |-  ( ( c X. d ) i^i ( _I |` X ) ) = ( ( c X. d ) i^i ( _I i^i ( X X. _V ) ) )
55 inass
 |-  ( ( ( c X. d ) i^i _I ) i^i ( X X. _V ) ) = ( ( c X. d ) i^i ( _I i^i ( X X. _V ) ) )
56 inss1
 |-  ( ( c X. d ) i^i _I ) C_ ( c X. d )
57 56 48 sstrid
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( c X. d ) i^i _I ) C_ ( X X. X ) )
58 ssv
 |-  X C_ _V
59 xpss2
 |-  ( X C_ _V -> ( X X. X ) C_ ( X X. _V ) )
60 58 59 ax-mp
 |-  ( X X. X ) C_ ( X X. _V )
61 57 60 sstrdi
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( c X. d ) i^i _I ) C_ ( X X. _V ) )
62 df-ss
 |-  ( ( ( c X. d ) i^i _I ) C_ ( X X. _V ) <-> ( ( ( c X. d ) i^i _I ) i^i ( X X. _V ) ) = ( ( c X. d ) i^i _I ) )
63 61 62 sylib
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( c X. d ) i^i _I ) i^i ( X X. _V ) ) = ( ( c X. d ) i^i _I ) )
64 55 63 eqtr3id
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( c X. d ) i^i ( _I i^i ( X X. _V ) ) ) = ( ( c X. d ) i^i _I ) )
65 54 64 syl5eq
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( c X. d ) i^i ( _I |` X ) ) = ( ( c X. d ) i^i _I ) )
66 65 eqeq1d
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( c X. d ) i^i ( _I |` X ) ) = (/) <-> ( ( c X. d ) i^i _I ) = (/) ) )
67 opelxp
 |-  ( <. a , a >. e. ( c X. d ) <-> ( a e. c /\ a e. d ) )
68 df-br
 |-  ( a ( c X. d ) a <-> <. a , a >. e. ( c X. d ) )
69 elin
 |-  ( a e. ( c i^i d ) <-> ( a e. c /\ a e. d ) )
70 67 68 69 3bitr4i
 |-  ( a ( c X. d ) a <-> a e. ( c i^i d ) )
71 70 notbii
 |-  ( -. a ( c X. d ) a <-> -. a e. ( c i^i d ) )
72 71 albii
 |-  ( A. a -. a ( c X. d ) a <-> A. a -. a e. ( c i^i d ) )
73 intirr
 |-  ( ( ( c X. d ) i^i _I ) = (/) <-> A. a -. a ( c X. d ) a )
74 eq0
 |-  ( ( c i^i d ) = (/) <-> A. a -. a e. ( c i^i d ) )
75 72 73 74 3bitr4i
 |-  ( ( ( c X. d ) i^i _I ) = (/) <-> ( c i^i d ) = (/) )
76 66 75 bitrdi
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( c X. d ) i^i ( _I |` X ) ) = (/) <-> ( c i^i d ) = (/) ) )
77 52 76 bitr3d
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) <-> ( c i^i d ) = (/) ) )
78 77 anbi2d
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> ( ( a e. c /\ b e. d ) /\ ( c i^i d ) = (/) ) ) )
79 opelxp
 |-  ( <. a , b >. e. ( c X. d ) <-> ( a e. c /\ b e. d ) )
80 79 anbi1i
 |-  ( ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) )
81 df-3an
 |-  ( ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) <-> ( ( a e. c /\ b e. d ) /\ ( c i^i d ) = (/) ) )
82 78 80 81 3bitr4g
 |-  ( ( ( J e. Top /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) )
83 82 2rexbidva
 |-  ( ( J e. Top /\ ( a e. X /\ b e. X ) ) -> ( E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) )
84 41 83 imbi12d
 |-  ( ( J e. Top /\ ( a e. X /\ b e. X ) ) -> ( ( -. <. a , b >. e. ( _I |` X ) -> E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> ( a =/= b -> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) ) )
85 84 2ralbidva
 |-  ( J e. Top -> ( A. a e. X A. b e. X ( -. <. a , b >. e. ( _I |` X ) -> E. c e. J E. d e. J ( <. a , b >. e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) ) <-> A. a e. X A. b e. X ( a =/= b -> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) ) )
86 30 85 bitrd
 |-  ( J e. Top -> ( A. e e. ( U. ( J tX J ) \ ( _I |` X ) ) E. c e. J E. d e. J ( e e. ( c X. d ) /\ ( c X. d ) C_ ( U. ( J tX J ) \ ( _I |` X ) ) ) <-> A. a e. X A. b e. X ( a =/= b -> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) ) )
87 11 13 86 3bitrrd
 |-  ( J e. Top -> ( A. a e. X A. b e. X ( a =/= b -> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) <-> ( _I |` X ) e. ( Clsd ` ( J tX J ) ) ) )
88 87 pm5.32i
 |-  ( ( J e. Top /\ A. a e. X A. b e. X ( a =/= b -> E. c e. J E. d e. J ( a e. c /\ b e. d /\ ( c i^i d ) = (/) ) ) ) <-> ( J e. Top /\ ( _I |` X ) e. ( Clsd ` ( J tX J ) ) ) )
89 2 88 bitri
 |-  ( J e. Haus <-> ( J e. Top /\ ( _I |` X ) e. ( Clsd ` ( J tX J ) ) ) )