Metamath Proof Explorer


Theorem cfilucfil2

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion cfilucfil2 ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 metuval ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
2 1 adantl ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
3 2 fveq2d ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) = ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) )
4 3 eleq2d ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) ) )
5 oveq2 ( 𝑎 = 𝑏 → ( 0 [,) 𝑎 ) = ( 0 [,) 𝑏 ) )
6 5 imaeq2d ( 𝑎 = 𝑏 → ( 𝐷 “ ( 0 [,) 𝑎 ) ) = ( 𝐷 “ ( 0 [,) 𝑏 ) ) )
7 6 cbvmptv ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑏 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑏 ) ) )
8 7 rneqi ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑏 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑏 ) ) )
9 8 cfilucfil ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
10 4 9 bitrd ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )