Metamath Proof Explorer

Theorem caufpm

Description: Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)

		Ref	Expression
	Assertion	caufpm	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to F \in (X ↑_{𝑝𝑚} ℂ)$

Step	Hyp	Ref	Expression
1		iscau	$⊢ D \in ∞Met (X) \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists y \in ℤ ({F ↾}_{ℤ_{\geq y}}) : ℤ_{\geq y} ⟶ F (y) ball (D) x))$
2	1	simprbda	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to F \in (X ↑_{𝑝𝑚} ℂ)$