caufval

Description: The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006) (Revised by Mario Carneiro, 5-Sep-2015)

		Ref	Expression
	Assertion	caufval	$⊢ D \in ∞Met (X) \to Cau (D) = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x\}$

Proof

Step	Hyp	Ref	Expression
1		df-cau	$⊢ Cau = (d \in ⋃ ran ∞Met ⟼ \{f \in (dom dom d ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (d) x\})$
2		dmeq	$⊢ d = D \to dom d = dom D$
3	2	dmeqd	$⊢ d = D \to dom dom d = dom dom D$
4		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
5	4	fdmd	$⊢ D \in ∞Met (X) \to dom D = X \times X$
6	5	dmeqd	$⊢ D \in ∞Met (X) \to dom dom D = dom (X \times X)$
7		dmxpid	$⊢ dom (X \times X) = X$
8	6 7	eqtrdi	$⊢ D \in ∞Met (X) \to dom dom D = X$
9	3 8	sylan9eqr	$⊢ (D \in ∞Met (X) \land d = D) \to dom dom d = X$
10	9	oveq1d	$⊢ (D \in ∞Met (X) \land d = D) \to dom dom d ↑_{𝑝𝑚} ℂ = X ↑_{𝑝𝑚} ℂ$
11		simpr	$⊢ (D \in ∞Met (X) \land d = D) \to d = D$
12	11	fveq2d	$⊢ (D \in ∞Met (X) \land d = D) \to ball (d) = ball (D)$
13	12	oveqd	$⊢ (D \in ∞Met (X) \land d = D) \to f (k) ball (d) x = f (k) ball (D) x$
14	13	feq3d	$⊢ (D \in ∞Met (X) \land d = D) \to (({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (d) x \leftrightarrow ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x)$
15	14	rexbidv	$⊢ (D \in ∞Met (X) \land d = D) \to (\exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (d) x \leftrightarrow \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x)$
16	15	ralbidv	$⊢ (D \in ∞Met (X) \land d = D) \to (\forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (d) x \leftrightarrow \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x)$
17	10 16	rabeqbidv	$⊢ (D \in ∞Met (X) \land d = D) \to \{f \in (dom dom d ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (d) x\} = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x\}$
18		fvssunirn	$⊢ ∞Met (X) \subseteq ⋃ ran ∞Met$
19	18	sseli	$⊢ D \in ∞Met (X) \to D \in ⋃ ran ∞Met$
20		ovex	$⊢ X ↑_{𝑝𝑚} ℂ \in V$
21	20	rabex	$⊢ \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x\} \in V$
22	21	a1i	$⊢ D \in ∞Met (X) \to \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x\} \in V$
23	1 17 19 22	fvmptd2	$⊢ D \in ∞Met (X) \to Cau (D) = \{f \in (X ↑_{𝑝𝑚} ℂ) \| \forall x \in ℝ^{+} \exists k \in ℤ ({f ↾}_{ℤ_{\geq k}}) : ℤ_{\geq k} ⟶ f (k) ball (D) x\}$

Metamath Proof Explorer

Theorem caufval

Proof