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 𝑋 = 𝐽
Assertion hausdiag ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ( I ↾ 𝑋 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )

Proof

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