lmcau

Description: Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of Kreyszig p. 28. (Contributed by NM, 29-Jan-2008) (Proof shortened by Mario Carneiro, 5-May-2014)

		Ref	Expression
	Hypothesis	lmcau.1	$⊢ J = MetOpen (D)$
	Assertion	lmcau	$⊢ D \in ∞Met (X) \to dom \underset{t}{⇝} (J) \subseteq Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		lmcau.1	$⊢ J = MetOpen (D)$
2	1	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$
3		lmfun	$⊢ J \in Haus \to Fun \underset{t}{⇝} (J)$
4		funfvbrb	$⊢ Fun \underset{t}{⇝} (J) \to (f \in dom \underset{t}{⇝} (J) \leftrightarrow f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f))$
5	2 3 4	3syl	$⊢ D \in ∞Met (X) \to (f \in dom \underset{t}{⇝} (J) \leftrightarrow f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f))$
6		id	$⊢ D \in ∞Met (X) \to D \in ∞Met (X)$
7	1 6	lmmbr	$⊢ D \in ∞Met (X) \to (f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f) \leftrightarrow (f \in (X ↑_{𝑝𝑚} ℂ) \land \underset{t}{⇝} (J) (f) \in X \land \forall y \in ℝ^{+} \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) y))$
8	7	biimpa	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to (f \in (X ↑_{𝑝𝑚} ℂ) \land \underset{t}{⇝} (J) (f) \in X \land \forall y \in ℝ^{+} \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) y)$
9	8	simp1d	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to f \in (X ↑_{𝑝𝑚} ℂ)$
10		simprr	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2})$
11		simplll	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to D \in ∞Met (X)$
12	8	simp2d	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to \underset{t}{⇝} (J) (f) \in X$
13	12	ad2antrr	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to \underset{t}{⇝} (J) (f) \in X$
14		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
15	14	ad2antlr	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to x \in ℝ$
16		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
17	16	ad2antrl	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to j \in ℤ_{\geq j}$
18	17	fvresd	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to ({f ↾}_{ℤ_{\geq j}}) (j) = f (j)$
19	10 17	ffvelrnd	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to ({f ↾}_{ℤ_{\geq j}}) (j) \in (\underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
20	18 19	eqeltrrd	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to f (j) \in (\underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
21		blhalf	$⊢ ((D \in ∞Met (X) \land \underset{t}{⇝} (J) (f) \in X) \land (x \in ℝ \land f (j) \in (\underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2})))) \to \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}) \subseteq f (j) ball (D) x$
22	11 13 15 20 21	syl22anc	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}) \subseteq f (j) ball (D) x$
23	10 22	fssd	$⊢ (((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \land (j \in ℤ \land ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))) \to ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ f (j) ball (D) x$
24		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
25	8	simp3d	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to \forall y \in ℝ^{+} \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) y$
26		oveq2	$⊢ y = \frac{x}{2} \to \underset{t}{⇝} (J) (f) ball (D) y = \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2})$
27	26	feq3d	$⊢ y = \frac{x}{2} \to (({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) y \leftrightarrow ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
28	27	rexbidv	$⊢ y = \frac{x}{2} \to (\exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) y \leftrightarrow \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
29	28	rspcv	$⊢ \frac{x}{2} \in ℝ^{+} \to (\forall y \in ℝ^{+} \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) y \to \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
30	24 25 29	syl2im	$⊢ x \in ℝ^{+} \to ((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
31	30	impcom	$⊢ ((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \to \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2})$
32		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
33		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
34		reseq2	$⊢ u = ℤ_{\geq j} \to {f ↾}_{u} = {f ↾}_{ℤ_{\geq j}}$
35		id	$⊢ u = ℤ_{\geq j} \to u = ℤ_{\geq j}$
36	34 35	feq12d	$⊢ u = ℤ_{\geq j} \to (({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}) \leftrightarrow ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
37	36	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}) \leftrightarrow \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}))$
38	32 33 37	mp2b	$⊢ \exists u \in ran ℤ_{\geq} ({f ↾}_{u}) : u ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2}) \leftrightarrow \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2})$
39	31 38	sylib	$⊢ ((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \to \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ \underset{t}{⇝} (J) (f) ball (D) (\frac{x}{2})$
40	23 39	reximddv	$⊢ ((D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \land x \in ℝ^{+}) \to \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ f (j) ball (D) x$
41	40	ralrimiva	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ f (j) ball (D) x$
42		iscau	$⊢ D \in ∞Met (X) \to (f \in Cau (D) \leftrightarrow (f \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ f (j) ball (D) x))$
43	42	adantr	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to (f \in Cau (D) \leftrightarrow (f \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ f (j) ball (D) x))$
44	9 41 43	mpbir2and	$⊢ (D \in ∞Met (X) \land f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f)) \to f \in Cau (D)$
45	44	ex	$⊢ D \in ∞Met (X) \to (f \underset{t}{⇝} (J) \underset{t}{⇝} (J) (f) \to f \in Cau (D))$
46	5 45	sylbid	$⊢ D \in ∞Met (X) \to (f \in dom \underset{t}{⇝} (J) \to f \in Cau (D))$
47	46	ssrdv	$⊢ D \in ∞Met (X) \to dom \underset{t}{⇝} (J) \subseteq Cau (D)$

Metamath Proof Explorer

Theorem lmcau

Proof