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 syl5eqr 
 |-  ( ( ( 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 ) ) ) )