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 ‘ 𝐷 ) ) )