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

Metamath Proof Explorer

Theorem cfilucfil3

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion cfilucfil3 ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 xmetpsmet ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2 cfilucfil2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
3 2 anbi2d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ) )
4 filfbas ⊢ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
5 4 pm4.71i ⊢ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑋 ) ) )
6 5 anbi1i ⊢ ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ↔ ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
7 anass ⊢ ( ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( fBas ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
8 6 7 bitr2i ⊢ ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
9 3 8 bitrdi ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
10 1 9 sylan2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
11 iscfil ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐶 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
12 11 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐶 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
13 10 12 bitr4d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) )