| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cmetmet |
⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
| 2 |
|
metxmet |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 3 |
|
xmetpsmet |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) |
| 4 |
1 2 3
|
3syl |
⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) |
| 5 |
4
|
anim2i |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ) |
| 6 |
|
metuust |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) ) |
| 7 |
|
eqid |
⊢ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) = ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) |
| 8 |
7
|
tususp |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ UnifSp ) |
| 9 |
5 6 8
|
3syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ UnifSp ) |
| 10 |
|
simpll |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ) |
| 11 |
10
|
simprd |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) ) |
| 12 |
1 2
|
syl |
⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 13 |
12
|
ad3antlr |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 14 |
7
|
tusbas |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) |
| 15 |
14
|
fveq2d |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( Fil ‘ 𝑋 ) = ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) |
| 16 |
15
|
eleq2d |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ↔ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ) |
| 17 |
5 6 16
|
3syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ↔ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ) |
| 18 |
17
|
biimpar |
⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( Fil ‘ 𝑋 ) ) |
| 19 |
18
|
adantr |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( Fil ‘ 𝑋 ) ) |
| 20 |
7
|
tususs |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) |
| 21 |
20
|
fveq2d |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) = ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) |
| 22 |
5 6 21
|
3syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) = ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) |
| 23 |
22
|
eleq2d |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ) |
| 24 |
23
|
biimpar |
⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) |
| 25 |
24
|
adantlr |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) |
| 26 |
|
cfilucfil2 |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝑐 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ) |
| 27 |
5 26
|
syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝑐 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ) |
| 28 |
27
|
simplbda |
⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) |
| 29 |
10 25 28
|
syl2anc |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) |
| 30 |
|
iscfil |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑐 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ) |
| 31 |
30
|
biimpar |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) |
| 32 |
13 19 29 31
|
syl12anc |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) |
| 33 |
|
eqid |
⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 ) |
| 34 |
33
|
cmetcvg |
⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) |
| 35 |
11 32 34
|
syl2anc |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) |
| 36 |
|
eqid |
⊢ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) |
| 37 |
7 36
|
tustopn |
⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) |
| 38 |
5 6 37
|
3syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) |
| 39 |
12
|
anim2i |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ) |
| 40 |
|
xmetutop |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) ) |
| 41 |
39 40
|
syl |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) ) |
| 42 |
38 41
|
eqtr3d |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) = ( MetOpen ‘ 𝐷 ) ) |
| 43 |
42
|
oveq1d |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) = ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ) |
| 44 |
43
|
neeq1d |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ↔ ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) ) |
| 45 |
44
|
biimpar |
⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) |
| 46 |
10 35 45
|
syl2anc |
⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) |
| 47 |
46
|
ex |
⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) ) |
| 48 |
47
|
ralrimiva |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) ) |
| 49 |
|
iscusp |
⊢ ( ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ CUnifSp ↔ ( ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) ) ) |
| 50 |
9 48 49
|
sylanbrc |
⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ CUnifSp ) |