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