caures

Description: The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	caures.1	$⊢ Z = ℤ_{\geq M}$
	caures.3	$⊢ φ \to M \in ℤ$
	caures.4	$⊢ φ \to D \in Met (X)$
	caures.5	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
Assertion	caures	$⊢ φ \to (F \in Cau (D) \leftrightarrow {F ↾}_{Z} \in Cau (D))$

Proof

Step	Hyp	Ref	Expression
1		caures.1	$⊢ Z = ℤ_{\geq M}$
2		caures.3	$⊢ φ \to M \in ℤ$
3		caures.4	$⊢ φ \to D \in Met (X)$
4		caures.5	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
5	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
6	5	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
7	6	biantrurd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (k \in dom F \leftrightarrow (k \in Z \land k \in dom F))$
8		dmres	$⊢ dom ({F ↾}_{Z}) = Z \cap dom F$
9	8	elin2	$⊢ k \in dom ({F ↾}_{Z}) \leftrightarrow (k \in Z \land k \in dom F)$
10	7 9	bitr4di	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (k \in dom F \leftrightarrow k \in dom ({F ↾}_{Z}))$
11	10	3anbi1d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x))$
12	11	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x))$
13	12	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x))$
14	13	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x))$
15	4	biantrurd	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
16		elfvdm	$⊢ D \in Met (X) \to X \in dom Met$
17	3 16	syl	$⊢ φ \to X \in dom Met$
18		cnex	$⊢ ℂ \in V$
19		ssid	$⊢ X \subseteq X$
20		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
21		zsscn	$⊢ ℤ \subseteq ℂ$
22	20 21	sstri	$⊢ ℤ_{\geq M} \subseteq ℂ$
23	1 22	eqsstri	$⊢ Z \subseteq ℂ$
24		pmss12g	$⊢ ((X \subseteq X \land Z \subseteq ℂ) \land (X \in dom Met \land ℂ \in V)) \to X ↑_{𝑝𝑚} Z \subseteq X ↑_{𝑝𝑚} ℂ$
25	19 23 24	mpanl12	$⊢ (X \in dom Met \land ℂ \in V) \to X ↑_{𝑝𝑚} Z \subseteq X ↑_{𝑝𝑚} ℂ$
26	17 18 25	sylancl	$⊢ φ \to X ↑_{𝑝𝑚} Z \subseteq X ↑_{𝑝𝑚} ℂ$
27	1	fvexi	$⊢ Z \in V$
28		pmresg	$⊢ (Z \in V \land F \in (X ↑_{𝑝𝑚} ℂ)) \to {F ↾}_{Z} \in (X ↑_{𝑝𝑚} Z)$
29	27 4 28	sylancr	$⊢ φ \to {F ↾}_{Z} \in (X ↑_{𝑝𝑚} Z)$
30	26 29	sseldd	$⊢ φ \to {F ↾}_{Z} \in (X ↑_{𝑝𝑚} ℂ)$
31	30	biantrurd	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow ({F ↾}_{Z} \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x)))$
32	14 15 31	3bitr3d	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \leftrightarrow ({F ↾}_{Z} \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x)))$
33		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
34	3 33	syl	$⊢ φ \to D \in ∞Met (X)$
35		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
36		eqidd	$⊢ (φ \land j \in Z) \to F (j) = F (j)$
37	1 34 2 35 36	iscau4	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
38		fvres	$⊢ k \in Z \to ({F ↾}_{Z}) (k) = F (k)$
39	38	adantl	$⊢ (φ \land k \in Z) \to ({F ↾}_{Z}) (k) = F (k)$
40		fvres	$⊢ j \in Z \to ({F ↾}_{Z}) (j) = F (j)$
41	40	adantl	$⊢ (φ \land j \in Z) \to ({F ↾}_{Z}) (j) = F (j)$
42	1 34 2 39 41	iscau4	$⊢ φ \to ({F ↾}_{Z} \in Cau (D) \leftrightarrow ({F ↾}_{Z} \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{Z}) \land F (k) \in X \land F (k) D F (j) < x)))$
43	32 37 42	3bitr4d	$⊢ φ \to (F \in Cau (D) \leftrightarrow {F ↾}_{Z} \in Cau (D))$

Metamath Proof Explorer

Theorem caures

Proof