Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) |
2 |
|
metdscn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
3 |
|
metnrmlem.1 |
⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
4 |
|
metnrmlem.2 |
⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) |
5 |
|
metnrmlem.3 |
⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) |
6 |
|
metnrmlem.4 |
⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ ) |
7 |
|
metnrmlem.u |
⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) |
8 |
2
|
mopntop |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top ) |
9 |
3 8
|
syl |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
10 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
11 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
12 |
11
|
cldss |
⊢ ( 𝑇 ∈ ( Clsd ‘ 𝐽 ) → 𝑇 ⊆ ∪ 𝐽 ) |
13 |
5 12
|
syl |
⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 ) |
14 |
2
|
mopnuni |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
15 |
3 14
|
syl |
⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 ) |
16 |
13 15
|
sseqtrrd |
⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 ) |
17 |
16
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑋 ) |
18 |
1 2 3 4 5 6
|
metnrmlem1a |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 < ( 𝐹 ‘ 𝑡 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ ) ) |
19 |
18
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ ) |
20 |
19
|
rphalfcld |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ+ ) |
21 |
20
|
rpxrd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ* ) |
22 |
2
|
blopn |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ∧ ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ* ) → ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) |
23 |
10 17 21 22
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) |
24 |
23
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) |
25 |
|
iunopn |
⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) → ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) |
26 |
9 24 25
|
syl2anc |
⊢ ( 𝜑 → ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) |
27 |
7 26
|
eqeltrid |
⊢ ( 𝜑 → 𝑈 ∈ 𝐽 ) |
28 |
|
blcntr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ∧ ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ+ ) → 𝑡 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) |
29 |
10 17 20 28
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) |
30 |
29
|
snssd |
⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → { 𝑡 } ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) |
31 |
30
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) |
32 |
|
ss2iun |
⊢ ( ∀ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) → ∪ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) |
33 |
31 32
|
syl |
⊢ ( 𝜑 → ∪ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) |
34 |
|
iunid |
⊢ ∪ 𝑡 ∈ 𝑇 { 𝑡 } = 𝑇 |
35 |
34
|
eqcomi |
⊢ 𝑇 = ∪ 𝑡 ∈ 𝑇 { 𝑡 } |
36 |
33 35 7
|
3sstr4g |
⊢ ( 𝜑 → 𝑇 ⊆ 𝑈 ) |
37 |
27 36
|
jca |
⊢ ( 𝜑 → ( 𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈 ) ) |