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 )