cfilucfil4

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	cfilucfil4	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cfilucfil3	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) )
2		cfilfil	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐶 ∈ ( Fil ‘ 𝑋 ) )
3	2	ex	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐶 ∈ ( CauFil ‘ 𝐷 ) → 𝐶 ∈ ( Fil ‘ 𝑋 ) ) )
4	3	adantl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil ‘ 𝐷 ) → 𝐶 ∈ ( Fil ‘ 𝑋 ) ) )
5	4	pm4.71rd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) ) )
6	1 5	bitrd	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) ) )
7		pm5.32	⊢ ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) → ( 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) ) ↔ ( ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ) ↔ ( 𝐶 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) ) )
8	6 7	sylibr	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐶 ∈ ( Fil ‘ 𝑋 ) → ( 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) ) )
9	8	3impia	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐶 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝐶 ∈ ( CauFil ‘ 𝐷 ) ) )

Metamath Proof Explorer

Theorem cfilucfil4

Proof