causs

Description: Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

		Ref	Expression
	Assertion	causs	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ Y) \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)}))$

Proof

Step	Hyp	Ref	Expression
1		caufpm	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to F \in (X ↑_{𝑝𝑚} ℂ)$
2		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
3		cnex	$⊢ ℂ \in V$
4		elpmg	$⊢ (X \in dom ∞Met \land ℂ \in V) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
5	2 3 4	sylancl	$⊢ D \in ∞Met (X) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
6	5	biimpa	$⊢ (D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to (Fun F \land F \subseteq ℂ \times X)$
7	1 6	syldan	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to (Fun F \land F \subseteq ℂ \times X)$
8		rnss	$⊢ F \subseteq ℂ \times X \to ran F \subseteq ran (ℂ \times X)$
9	7 8	simpl2im	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to ran F \subseteq ran (ℂ \times X)$
10		rnxpss	$⊢ ran (ℂ \times X) \subseteq X$
11	9 10	sstrdi	$⊢ (D \in ∞Met (X) \land F \in Cau (D)) \to ran F \subseteq X$
12	11	adantlr	$⊢ ((D \in ∞Met (X) \land F : ℕ ⟶ Y) \land F \in Cau (D)) \to ran F \subseteq X$
13		frn	$⊢ F : ℕ ⟶ Y \to ran F \subseteq Y$
14	13	ad2antlr	$⊢ ((D \in ∞Met (X) \land F : ℕ ⟶ Y) \land F \in Cau (D)) \to ran F \subseteq Y$
15	12 14	ssind	$⊢ ((D \in ∞Met (X) \land F : ℕ ⟶ Y) \land F \in Cau (D)) \to ran F \subseteq X \cap Y$
16	15	ex	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ Y) \to (F \in Cau (D) \to ran F \subseteq X \cap Y)$
17		xmetres	$⊢ D \in ∞Met (X) \to {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y)$
18		caufpm	$⊢ ({D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y) \land F \in Cau ({D ↾}_{(Y \times Y)})) \to F \in ((X \cap Y) ↑_{𝑝𝑚} ℂ)$
19	17 18	sylan	$⊢ (D \in ∞Met (X) \land F \in Cau ({D ↾}_{(Y \times Y)})) \to F \in ((X \cap Y) ↑_{𝑝𝑚} ℂ)$
20		inex1g	$⊢ X \in dom ∞Met \to X \cap Y \in V$
21	2 20	syl	$⊢ D \in ∞Met (X) \to X \cap Y \in V$
22		elpmg	$⊢ (X \cap Y \in V \land ℂ \in V) \to (F \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times (X \cap Y)))$
23	21 3 22	sylancl	$⊢ D \in ∞Met (X) \to (F \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times (X \cap Y)))$
24	23	biimpa	$⊢ (D \in ∞Met (X) \land F \in ((X \cap Y) ↑_{𝑝𝑚} ℂ)) \to (Fun F \land F \subseteq ℂ \times (X \cap Y))$
25	19 24	syldan	$⊢ (D \in ∞Met (X) \land F \in Cau ({D ↾}_{(Y \times Y)})) \to (Fun F \land F \subseteq ℂ \times (X \cap Y))$
26		rnss	$⊢ F \subseteq ℂ \times (X \cap Y) \to ran F \subseteq ran (ℂ \times (X \cap Y))$
27	25 26	simpl2im	$⊢ (D \in ∞Met (X) \land F \in Cau ({D ↾}_{(Y \times Y)})) \to ran F \subseteq ran (ℂ \times (X \cap Y))$
28		rnxpss	$⊢ ran (ℂ \times (X \cap Y)) \subseteq X \cap Y$
29	27 28	sstrdi	$⊢ (D \in ∞Met (X) \land F \in Cau ({D ↾}_{(Y \times Y)})) \to ran F \subseteq X \cap Y$
30	29	ex	$⊢ D \in ∞Met (X) \to (F \in Cau ({D ↾}_{(Y \times Y)}) \to ran F \subseteq X \cap Y)$
31	30	adantr	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ Y) \to (F \in Cau ({D ↾}_{(Y \times Y)}) \to ran F \subseteq X \cap Y)$
32		ffn	$⊢ F : ℕ ⟶ Y \to F Fn ℕ$
33		df-f	$⊢ F : ℕ ⟶ X \cap Y \leftrightarrow (F Fn ℕ \land ran F \subseteq X \cap Y)$
34	33	simplbi2	$⊢ F Fn ℕ \to (ran F \subseteq X \cap Y \to F : ℕ ⟶ X \cap Y)$
35	32 34	syl	$⊢ F : ℕ ⟶ Y \to (ran F \subseteq X \cap Y \to F : ℕ ⟶ X \cap Y)$
36		inss2	$⊢ X \cap Y \subseteq Y$
37	36	a1i	$⊢ D \in ∞Met (X) \to X \cap Y \subseteq Y$
38		fss	$⊢ (F : ℕ ⟶ X \cap Y \land X \cap Y \subseteq Y) \to F : ℕ ⟶ Y$
39	37 38	sylan2	$⊢ (F : ℕ ⟶ X \cap Y \land D \in ∞Met (X)) \to F : ℕ ⟶ Y$
40	39	ancoms	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to F : ℕ ⟶ Y$
41		ffvelrn	$⊢ (F : ℕ ⟶ Y \land y \in ℕ) \to F (y) \in Y$
42	41	adantr	$⊢ ((F : ℕ ⟶ Y \land y \in ℕ) \land z \in ℤ_{\geq y}) \to F (y) \in Y$
43		eluznn	$⊢ (y \in ℕ \land z \in ℤ_{\geq y}) \to z \in ℕ$
44		ffvelrn	$⊢ (F : ℕ ⟶ Y \land z \in ℕ) \to F (z) \in Y$
45	43 44	sylan2	$⊢ (F : ℕ ⟶ Y \land (y \in ℕ \land z \in ℤ_{\geq y})) \to F (z) \in Y$
46	45	anassrs	$⊢ ((F : ℕ ⟶ Y \land y \in ℕ) \land z \in ℤ_{\geq y}) \to F (z) \in Y$
47	42 46	ovresd	$⊢ ((F : ℕ ⟶ Y \land y \in ℕ) \land z \in ℤ_{\geq y}) \to F (y) ({D ↾}_{(Y \times Y)}) F (z) = F (y) D F (z)$
48	47	breq1d	$⊢ ((F : ℕ ⟶ Y \land y \in ℕ) \land z \in ℤ_{\geq y}) \to (F (y) ({D ↾}_{(Y \times Y)}) F (z) < x \leftrightarrow F (y) D F (z) < x)$
49	48	ralbidva	$⊢ (F : ℕ ⟶ Y \land y \in ℕ) \to (\forall z \in ℤ_{\geq y} F (y) ({D ↾}_{(Y \times Y)}) F (z) < x \leftrightarrow \forall z \in ℤ_{\geq y} F (y) D F (z) < x)$
50	49	rexbidva	$⊢ F : ℕ ⟶ Y \to (\exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) ({D ↾}_{(Y \times Y)}) F (z) < x \leftrightarrow \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) D F (z) < x)$
51	50	ralbidv	$⊢ F : ℕ ⟶ Y \to (\forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) ({D ↾}_{(Y \times Y)}) F (z) < x \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) D F (z) < x)$
52	40 51	syl	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to (\forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) ({D ↾}_{(Y \times Y)}) F (z) < x \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) D F (z) < x)$
53		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
54	17	adantr	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y)$
55		1zzd	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to 1 \in ℤ$
56		eqidd	$⊢ ((D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \land z \in ℕ) \to F (z) = F (z)$
57		eqidd	$⊢ ((D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \land y \in ℕ) \to F (y) = F (y)$
58		simpr	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to F : ℕ ⟶ X \cap Y$
59	53 54 55 56 57 58	iscauf	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to (F \in Cau ({D ↾}_{(Y \times Y)}) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) ({D ↾}_{(Y \times Y)}) F (z) < x)$
60		simpl	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to D \in ∞Met (X)$
61		id	$⊢ F : ℕ ⟶ X \cap Y \to F : ℕ ⟶ X \cap Y$
62		inss1	$⊢ X \cap Y \subseteq X$
63	62	a1i	$⊢ D \in ∞Met (X) \to X \cap Y \subseteq X$
64		fss	$⊢ (F : ℕ ⟶ X \cap Y \land X \cap Y \subseteq X) \to F : ℕ ⟶ X$
65	61 63 64	syl2anr	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to F : ℕ ⟶ X$
66	53 60 55 56 57 65	iscauf	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℕ \forall z \in ℤ_{\geq y} F (y) D F (z) < x)$
67	52 59 66	3bitr4rd	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ X \cap Y) \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)}))$
68	67	ex	$⊢ D \in ∞Met (X) \to (F : ℕ ⟶ X \cap Y \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)})))$
69	35 68	sylan9r	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ Y) \to (ran F \subseteq X \cap Y \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)})))$
70	16 31 69	pm5.21ndd	$⊢ (D \in ∞Met (X) \land F : ℕ ⟶ Y) \to (F \in Cau (D) \leftrightarrow F \in Cau ({D ↾}_{(Y \times Y)}))$

Metamath Proof Explorer

Theorem causs

Proof