This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝐽 ∈ 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 bitrid ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 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 dfss2 ⊢ ( ( ( 𝑐 × 𝑑 ) ∩ I ) ⊆ ( 𝑋 × V ) ↔ ( ( ( 𝑐 × 𝑑 ) ∩ I ) ∩ ( 𝑋 × V ) ) = ( ( 𝑐 × 𝑑 ) ∩ I ) )
63 61 62 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ) → ( ( ( 𝑐 × 𝑑 ) ∩ I ) ∩ ( 𝑋 × V ) ) = ( ( 𝑐 × 𝑑 ) ∩ I ) )
64 55 63 eqtr3id ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽 ) ) → ( ( 𝑐 × 𝑑 ) ∩ ( I ∩ ( 𝑋 × V ) ) ) = ( ( 𝑐 × 𝑑 ) ∩ I ) )
65 54 64 eqtrid ⊢ ( ( ( 𝐽 ∈ 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 𝐽 ) ) ) )