Metamath Proof Explorer

Theorem methaus

Description: The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis methaus.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion methaus ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )

Proof

Step Hyp Ref Expression
1 methaus.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopnex ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∃ 𝑑 ∈ ( Met ‘ 𝑋 ) 𝐽 = ( MetOpen ‘ 𝑑 ) )
3 metxmet ⊢ ( 𝑑 ∈ ( Met ‘ 𝑋 ) → 𝑑 ∈ ( ∞Met ‘ 𝑋 ) )
4 3 ad2antrr ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑑 ∈ ( ∞Met ‘ 𝑋 ) )
5 simplrl ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ 𝑋 )
6 metcl ⊢ ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑑 𝑦 ) ∈ ℝ )
7 6 3expb ⊢ ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑑 𝑦 ) ∈ ℝ )
8 7 adantr ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝑑 𝑦 ) ∈ ℝ )
9 metgt0 ⊢ ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ≠ 𝑦 ↔ 0 < ( 𝑥 𝑑 𝑦 ) ) )
10 9 3expb ⊢ ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ≠ 𝑦 ↔ 0 < ( 𝑥 𝑑 𝑦 ) ) )
11 10 biimpa ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → 0 < ( 𝑥 𝑑 𝑦 ) )
12 8 11 elrpd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝑑 𝑦 ) ∈ ℝ+ )
13 12 rphalfcld ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ+ )
14 13 rpxrd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ* )
15 eqid ⊢ ( MetOpen ‘ 𝑑 ) = ( MetOpen ‘ 𝑑 )
16 15 blopn ⊢ ( ( 𝑑 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∈ ( MetOpen ‘ 𝑑 ) )
17 4 5 14 16 syl3anc ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∈ ( MetOpen ‘ 𝑑 ) )
18 simplrr ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ 𝑋 )
19 15 blopn ⊢ ( ( 𝑑 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∈ ( MetOpen ‘ 𝑑 ) )
20 4 18 14 19 syl3anc ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∈ ( MetOpen ‘ 𝑑 ) )
21 blcntr ⊢ ( ( 𝑑 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) )
22 4 5 13 21 syl3anc ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) )
23 blcntr ⊢ ( ( 𝑑 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ+ ) → 𝑦 ∈ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) )
24 4 18 13 23 syl3anc ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) )
25 13 rpred ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ )
26 25 25 rexaddd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) +𝑒 ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) = ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) + ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) )
27 8 recnd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝑑 𝑦 ) ∈ ℂ )
28 27 2halvesd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) + ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) = ( 𝑥 𝑑 𝑦 ) )
29 26 28 eqtrd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) +𝑒 ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) = ( 𝑥 𝑑 𝑦 ) )
30 8 leidd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝑑 𝑦 ) ≤ ( 𝑥 𝑑 𝑦 ) )
31 29 30 eqbrtrd ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) +𝑒 ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ≤ ( 𝑥 𝑑 𝑦 ) )
32 bldisj ⊢ ( ( ( 𝑑 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ* ∧ ( ( 𝑥 𝑑 𝑦 ) / 2 ) ∈ ℝ* ∧ ( ( ( 𝑥 𝑑 𝑦 ) / 2 ) +𝑒 ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ≤ ( 𝑥 𝑑 𝑦 ) ) ) → ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) = ∅ )
33 4 5 18 14 14 31 32 syl33anc ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) = ∅ )
34 eleq2 ⊢ ( 𝑚 = ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( 𝑥 ∈ 𝑚 ↔ 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) )
35 ineq1 ⊢ ( 𝑚 = ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( 𝑚 ∩ 𝑛 ) = ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ 𝑛 ) )
36 35 eqeq1d ⊢ ( 𝑚 = ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ 𝑛 ) = ∅ ) )
37 34 36 3anbi13d ⊢ ( 𝑚 = ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∧ 𝑦 ∈ 𝑛 ∧ ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ 𝑛 ) = ∅ ) ) )
38 eleq2 ⊢ ( 𝑛 = ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( 𝑦 ∈ 𝑛 ↔ 𝑦 ∈ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) )
39 ineq2 ⊢ ( 𝑛 = ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ 𝑛 ) = ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) )
40 39 eqeq1d ⊢ ( 𝑛 = ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ 𝑛 ) = ∅ ↔ ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) = ∅ ) )
41 38 40 3anbi23d ⊢ ( 𝑛 = ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) → ( ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∧ 𝑦 ∈ 𝑛 ∧ ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ 𝑛 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∧ 𝑦 ∈ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∧ ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) = ∅ ) ) )
42 37 41 rspc2ev ⊢ ( ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∈ ( MetOpen ‘ 𝑑 ) ∧ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∈ ( MetOpen ‘ 𝑑 ) ∧ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∧ 𝑦 ∈ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∧ ( ( 𝑥 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝑑 ) ( ( 𝑥 𝑑 𝑦 ) / 2 ) ) ) = ∅ ) ) → ∃ 𝑚 ∈ ( MetOpen ‘ 𝑑 ) ∃ 𝑛 ∈ ( MetOpen ‘ 𝑑 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
43 17 20 22 24 33 42 syl113anc ⊢ ( ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑚 ∈ ( MetOpen ‘ 𝑑 ) ∃ 𝑛 ∈ ( MetOpen ‘ 𝑑 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
44 43 ex ⊢ ( ( 𝑑 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( MetOpen ‘ 𝑑 ) ∃ 𝑛 ∈ ( MetOpen ‘ 𝑑 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
45 44 ralrimivva ⊢ ( 𝑑 ∈ ( Met ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( MetOpen ‘ 𝑑 ) ∃ 𝑛 ∈ ( MetOpen ‘ 𝑑 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
46 15 mopntopon ⊢ ( 𝑑 ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ 𝑑 ) ∈ ( TopOn ‘ 𝑋 ) )
47 ishaus2 ⊢ ( ( MetOpen ‘ 𝑑 ) ∈ ( TopOn ‘ 𝑋 ) → ( ( MetOpen ‘ 𝑑 ) ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( MetOpen ‘ 𝑑 ) ∃ 𝑛 ∈ ( MetOpen ‘ 𝑑 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
48 3 46 47 3syl ⊢ ( 𝑑 ∈ ( Met ‘ 𝑋 ) → ( ( MetOpen ‘ 𝑑 ) ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ ( MetOpen ‘ 𝑑 ) ∃ 𝑛 ∈ ( MetOpen ‘ 𝑑 ) ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
49 45 48 mpbird ⊢ ( 𝑑 ∈ ( Met ‘ 𝑋 ) → ( MetOpen ‘ 𝑑 ) ∈ Haus )
50 eleq1 ⊢ ( 𝐽 = ( MetOpen ‘ 𝑑 ) → ( 𝐽 ∈ Haus ↔ ( MetOpen ‘ 𝑑 ) ∈ Haus ) )
51 49 50 syl5ibrcom ⊢ ( 𝑑 ∈ ( Met ‘ 𝑋 ) → ( 𝐽 = ( MetOpen ‘ 𝑑 ) → 𝐽 ∈ Haus ) )
52 51 rexlimiv ⊢ ( ∃ 𝑑 ∈ ( Met ‘ 𝑋 ) 𝐽 = ( MetOpen ‘ 𝑑 ) → 𝐽 ∈ Haus )
53 2 52 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )