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 \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to G \in CauFil (D)$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to G \in Fil (X)$
2		simprr	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to F \subseteq G$
3		iscfil	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in F D [y \times y] \subseteq [0, x)))$
4	3	simplbda	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to \forall x \in ℝ^{+} \exists y \in F D [y \times y] \subseteq [0, x)$
5	4	adantr	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to \forall x \in ℝ^{+} \exists y \in F D [y \times y] \subseteq [0, x)$
6		ssrexv	$⊢ F \subseteq G \to (\exists y \in F D [y \times y] \subseteq [0, x) \to \exists y \in G D [y \times y] \subseteq [0, x))$
7	6	ralimdv	$⊢ F \subseteq G \to (\forall x \in ℝ^{+} \exists y \in F D [y \times y] \subseteq [0, x) \to \forall x \in ℝ^{+} \exists y \in G D [y \times y] \subseteq [0, x))$
8	2 5 7	sylc	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to \forall x \in ℝ^{+} \exists y \in G D [y \times y] \subseteq [0, x)$
9		iscfil	$⊢ D \in ∞Met (X) \to (G \in CauFil (D) \leftrightarrow (G \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in G D [y \times y] \subseteq [0, x)))$
10	9	ad2antrr	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to (G \in CauFil (D) \leftrightarrow (G \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in G D [y \times y] \subseteq [0, x)))$
11	1 8 10	mpbir2and	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D)) \land (G \in Fil (X) \land F \subseteq G)) \to G \in CauFil (D)$