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

Metamath Proof Explorer

Theorem caun0

Description: A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)

		Ref	Expression
	Assertion	caun0	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to X \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		1rp	$⊢ 1 \in ℝ^{+}$
2	1	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
3		iscau2	$⊢ D \in ∞Met (X) \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
4	3	simplbda	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
5		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \to \exists x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
6	2 4 5	sylancr	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to \exists x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
7		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
8		ne0i	$⊢ j \in ℤ_{\geq j} \to ℤ_{\geq j} \neq \emptyset$
9		r19.2z	$⊢ (ℤ_{\geq j} \neq \emptyset \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \to \exists k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
10	9	ex	$⊢ ℤ_{\geq j} \neq \emptyset \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to \exists k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
11	7 8 10	3syl	$⊢ j \in ℤ \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to \exists k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
12		ne0i	$⊢ F (k) \in X \to X \neq \emptyset$
13	12	3ad2ant2	$⊢ (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to X \neq \emptyset$
14	13	rexlimivw	$⊢ \exists k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to X \neq \emptyset$
15	11 14	syl6	$⊢ j \in ℤ \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to X \neq \emptyset)$
16	15	rexlimiv	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to X \neq \emptyset$
17	16	rexlimivw	$⊢ \exists x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to X \neq \emptyset$
18	6 17	syl	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to X \neq \emptyset$