This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmetcusp

Description: The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion cmetcusp ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ CUnifSp )

Proof

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 )