Metamath Proof Explorer

Theorem cmetcau

Description: The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Oct-2015)

		Ref	Expression
	Hypothesis	cmetcau.1	$⊢ J = MetOpen (D)$
	Assertion	cmetcau	$⊢ (D \in CMet (X) \land F \in Cau (D)) \to F \in dom \underset{t}{⇝} (J)$

Proof

Step	Hyp	Ref	Expression
1		cmetcau.1	$⊢ J = MetOpen (D)$
2		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
3		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
4	2 3	syl	$⊢ D \in CMet (X) \to D \in ∞Met (X)$
5		caun0	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to X \neq \emptyset$
6	4 5	sylan	$⊢ (D \in CMet (X) \land F \in Cau (D)) \to X \neq \emptyset$
7		n0	$⊢ X \neq \emptyset \leftrightarrow \exists x x \in X$
8	6 7	sylib	$⊢ (D \in CMet (X) \land F \in Cau (D)) \to \exists x x \in X$
9		simpll	$⊢ ((D \in CMet (X) \land F \in Cau (D)) \land x \in X) \to D \in CMet (X)$
10		simpr	$⊢ ((D \in CMet (X) \land F \in Cau (D)) \land x \in X) \to x \in X$
11		simplr	$⊢ ((D \in CMet (X) \land F \in Cau (D)) \land x \in X) \to F \in Cau (D)$
12		eqid	$⊢ (y \in ℕ ⟼ if (y \in dom F, F (y), x)) = (y \in ℕ ⟼ if (y \in dom F, F (y), x))$
13	1 9 10 11 12	cmetcaulem	$⊢ ((D \in CMet (X) \land F \in Cau (D)) \land x \in X) \to F \in dom \underset{t}{⇝} (J)$
14	8 13	exlimddv	$⊢ (D \in CMet (X) \land F \in Cau (D)) \to F \in dom \underset{t}{⇝} (J)$