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

Metamath Proof Explorer

Theorem iscfil

Description: The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion iscfil ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 cfilfval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( CauFil ‘ 𝐷 ) = { 𝑓 ∈ ( Fil ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
2 1 eleq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( Fil ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } ) )
3 rexeq ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
4 3 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
5 4 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( Fil ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
6 2 5 bitrdi ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )