caussi

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

		Ref	Expression
	Assertion	caussi	$⊢ D \in ∞Met (X) \to Cau ({D ↾}_{(Y \times Y)}) \subseteq Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ X \cap Y \subseteq X$
2		xpss2	$⊢ X \cap Y \subseteq X \to ℂ \times (X \cap Y) \subseteq ℂ \times X$
3	1 2	ax-mp	$⊢ ℂ \times (X \cap Y) \subseteq ℂ \times X$
4		sstr	$⊢ (f \subseteq ℂ \times (X \cap Y) \land ℂ \times (X \cap Y) \subseteq ℂ \times X) \to f \subseteq ℂ \times X$
5	3 4	mpan2	$⊢ f \subseteq ℂ \times (X \cap Y) \to f \subseteq ℂ \times X$
6	5	anim2i	$⊢ (Fun f \land f \subseteq ℂ \times (X \cap Y)) \to (Fun f \land f \subseteq ℂ \times X)$
7	6	a1i	$⊢ D \in ∞Met (X) \to ((Fun f \land f \subseteq ℂ \times (X \cap Y)) \to (Fun f \land f \subseteq ℂ \times X))$
8		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
9		inex1g	$⊢ X \in dom ∞Met \to X \cap Y \in V$
10	8 9	syl	$⊢ D \in ∞Met (X) \to X \cap Y \in V$
11		cnex	$⊢ ℂ \in V$
12		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)))$
13	10 11 12	sylancl	$⊢ D \in ∞Met (X) \to (f \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun f \land f \subseteq ℂ \times (X \cap Y)))$
14		elpmg	$⊢ (X \in dom ∞Met \land ℂ \in V) \to (f \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun f \land f \subseteq ℂ \times X))$
15	8 11 14	sylancl	$⊢ D \in ∞Met (X) \to (f \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun f \land f \subseteq ℂ \times X))$
16	7 13 15	3imtr4d	$⊢ D \in ∞Met (X) \to (f \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \to f \in (X ↑_{𝑝𝑚} ℂ))$
17		uzid	$⊢ y \in ℤ \to y \in ℤ_{\geq y}$
18	17	adantl	$⊢ (D \in ∞Met (X) \land y \in ℤ) \to y \in ℤ_{\geq y}$
19		simp2	$⊢ (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to f (z) \in (X \cap Y)$
20	19	ralimi	$⊢ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to \forall z \in ℤ_{\geq y} f (z) \in (X \cap Y)$
21		fveq2	$⊢ z = y \to f (z) = f (y)$
22	21	eleq1d	$⊢ z = y \to (f (z) \in (X \cap Y) \leftrightarrow f (y) \in (X \cap Y))$
23	22	rspcva	$⊢ (y \in ℤ_{\geq y} \land \forall z \in ℤ_{\geq y} f (z) \in (X \cap Y)) \to f (y) \in (X \cap Y)$
24	18 20 23	syl2an	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)) \to f (y) \in (X \cap Y)$
25		simpr	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in (X \cap Y)) \to f (y) \in (X \cap Y)$
26	25	elin2d	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in (X \cap Y)) \to f (y) \in Y$
27		inss2	$⊢ X \cap Y \subseteq Y$
28	27	a1i	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \to X \cap Y \subseteq Y$
29	28	sselda	$⊢ (((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \land f (z) \in (X \cap Y)) \to f (z) \in Y$
30		simplr	$⊢ (((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \land f (z) \in (X \cap Y)) \to f (y) \in Y$
31	29 30	ovresd	$⊢ (((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \land f (z) \in (X \cap Y)) \to f (z) ({D ↾}_{(Y \times Y)}) f (y) = f (z) D f (y)$
32	31	breq1d	$⊢ (((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \land f (z) \in (X \cap Y)) \to (f (z) ({D ↾}_{(Y \times Y)}) f (y) < x \leftrightarrow f (z) D f (y) < x)$
33	32	biimpd	$⊢ (((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \land f (z) \in (X \cap Y)) \to (f (z) ({D ↾}_{(Y \times Y)}) f (y) < x \to f (z) D f (y) < x)$
34	33	imdistanda	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \to ((f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to (f (z) \in (X \cap Y) \land f (z) D f (y) < x))$
35	1	a1i	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \to X \cap Y \subseteq X$
36	35	sseld	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \to (f (z) \in (X \cap Y) \to f (z) \in X)$
37	36	anim1d	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \to ((f (z) \in (X \cap Y) \land f (z) D f (y) < x) \to (f (z) \in X \land f (z) D f (y) < x))$
38	34 37	syld	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in Y) \to ((f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to (f (z) \in X \land f (z) D f (y) < x))$
39	26 38	syldan	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in (X \cap Y)) \to ((f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to (f (z) \in X \land f (z) D f (y) < x))$
40	39	anim2d	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in (X \cap Y)) \to ((z \in dom f \land (f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)) \to (z \in dom f \land (f (z) \in X \land f (z) D f (y) < x)))$
41		3anass	$⊢ (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \leftrightarrow (z \in dom f \land (f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x))$
42		3anass	$⊢ (z \in dom f \land f (z) \in X \land f (z) D f (y) < x) \leftrightarrow (z \in dom f \land (f (z) \in X \land f (z) D f (y) < x))$
43	40 41 42	3imtr4g	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in (X \cap Y)) \to ((z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to (z \in dom f \land f (z) \in X \land f (z) D f (y) < x))$
44	43	ralimdv	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land f (y) \in (X \cap Y)) \to (\forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x))$
45	44	impancom	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)) \to (f (y) \in (X \cap Y) \to \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x))$
46	24 45	mpd	$⊢ ((D \in ∞Met (X) \land y \in ℤ) \land \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)) \to \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x)$
47	46	ex	$⊢ (D \in ∞Met (X) \land y \in ℤ) \to (\forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x))$
48	47	reximdva	$⊢ D \in ∞Met (X) \to (\exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x))$
49	48	ralimdv	$⊢ D \in ∞Met (X) \to (\forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x) \to \forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x))$
50	16 49	anim12d	$⊢ D \in ∞Met (X) \to ((f \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)) \to (f \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x)))$
51		xmetres	$⊢ D \in ∞Met (X) \to {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y)$
52		iscau2	$⊢ {D ↾}_{(Y \times Y)} \in ∞Met (X \cap Y) \to (f \in Cau ({D ↾}_{(Y \times Y)}) \leftrightarrow (f \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)))$
53	51 52	syl	$⊢ D \in ∞Met (X) \to (f \in Cau ({D ↾}_{(Y \times Y)}) \leftrightarrow (f \in ((X \cap Y) ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in (X \cap Y) \land f (z) ({D ↾}_{(Y \times Y)}) f (y) < x)))$
54		iscau2	$⊢ D \in ∞Met (X) \to (f \in Cau (D) \leftrightarrow (f \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists y \in ℤ \forall z \in ℤ_{\geq y} (z \in dom f \land f (z) \in X \land f (z) D f (y) < x)))$
55	50 53 54	3imtr4d	$⊢ D \in ∞Met (X) \to (f \in Cau ({D ↾}_{(Y \times Y)}) \to f \in Cau (D))$
56	55	ssrdv	$⊢ D \in ∞Met (X) \to Cau ({D ↾}_{(Y \times Y)}) \subseteq Cau (D)$

Metamath Proof Explorer

Theorem caussi

Proof