Metamath Proof Explorer

Theorem cfili

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

Ref Expression
Assertion cfili ⊢ F ∈ CauFil ⁡ D ∧ R ∈ ℝ + → ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < R

Proof

Step Hyp Ref Expression
1 df-cfil ⊢ CauFil = d ∈ ⋃ ran ⁡ ∞Met ⟼ f ∈ Fil ⁡ dom ⁡ dom ⁡ d | ∀ x ∈ ℝ + ∃ y ∈ f d y × y ⊆ 0 x
2 1 mptrcl ⊢ F ∈ CauFil ⁡ D → D ∈ ⋃ ran ⁡ ∞Met
3 xmetunirn ⊢ D ∈ ⋃ ran ⁡ ∞Met ↔ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
4 2 3 sylib ⊢ F ∈ CauFil ⁡ D → D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
5 iscfil2 ⊢ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D → F ∈ CauFil ⁡ D ↔ F ∈ Fil ⁡ dom ⁡ dom ⁡ D ∧ ∀ r ∈ ℝ + ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < r
6 4 5 syl ⊢ F ∈ CauFil ⁡ D → F ∈ CauFil ⁡ D ↔ F ∈ Fil ⁡ dom ⁡ dom ⁡ D ∧ ∀ r ∈ ℝ + ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < r
7 6 ibi ⊢ F ∈ CauFil ⁡ D → F ∈ Fil ⁡ dom ⁡ dom ⁡ D ∧ ∀ r ∈ ℝ + ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < r
8 7 simprd ⊢ F ∈ CauFil ⁡ D → ∀ r ∈ ℝ + ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < r
9 breq2 ⊢ r = R → y D z < r ↔ y D z < R
10 9 2ralbidv ⊢ r = R → ∀ y ∈ x ∀ z ∈ x y D z < r ↔ ∀ y ∈ x ∀ z ∈ x y D z < R
11 10 rexbidv ⊢ r = R → ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < r ↔ ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < R
12 11 rspccva ⊢ ∀ r ∈ ℝ + ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < r ∧ R ∈ ℝ + → ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < R
13 8 12 sylan ⊢ F ∈ CauFil ⁡ D ∧ R ∈ ℝ + → ∃ x ∈ F ∀ y ∈ x ∀ z ∈ x y D z < R