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

Metamath Proof Explorer

Theorem cfilss

Description: A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion cfilss ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → G ∈ CauFil ⁡ D

Proof

Step Hyp Ref Expression
1 simprl ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → G ∈ Fil ⁡ X
2 simprr ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → F ⊆ G
3 iscfil ⊢ D ∈ ∞Met ⁡ X → F ∈ CauFil ⁡ D ↔ F ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ F D y × y ⊆ 0 x
4 3 simplbda ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D → ∀ x ∈ ℝ + ∃ y ∈ F D y × y ⊆ 0 x
5 4 adantr ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → ∀ x ∈ ℝ + ∃ y ∈ F D y × y ⊆ 0 x
6 ssrexv ⊢ F ⊆ G → ∃ y ∈ F D y × y ⊆ 0 x → ∃ y ∈ G D y × y ⊆ 0 x
7 6 ralimdv ⊢ F ⊆ G → ∀ x ∈ ℝ + ∃ y ∈ F D y × y ⊆ 0 x → ∀ x ∈ ℝ + ∃ y ∈ G D y × y ⊆ 0 x
8 2 5 7 sylc ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → ∀ x ∈ ℝ + ∃ y ∈ G D y × y ⊆ 0 x
9 iscfil ⊢ D ∈ ∞Met ⁡ X → G ∈ CauFil ⁡ D ↔ G ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ G D y × y ⊆ 0 x
10 9 ad2antrr ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → G ∈ CauFil ⁡ D ↔ G ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ G D y × y ⊆ 0 x
11 1 8 10 mpbir2and ⊢ D ∈ ∞Met ⁡ X ∧ F ∈ CauFil ⁡ D ∧ G ∈ Fil ⁡ X ∧ F ⊆ G → G ∈ CauFil ⁡ D