lmres

Description: A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013)

	Ref	Expression
Hypotheses	lmres.2	$⊢ φ \to J \in TopOn (X)$
	lmres.4	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
	lmres.5	$⊢ φ \to M \in ℤ$
Assertion	lmres	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow ({F ↾}_{ℤ_{\geq M}}) \underset{t}{⇝} (J) P)$

Proof

Step	Hyp	Ref	Expression
1		lmres.2	$⊢ φ \to J \in TopOn (X)$
2		lmres.4	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
3		lmres.5	$⊢ φ \to M \in ℤ$
4		toponmax	$⊢ J \in TopOn (X) \to X \in J$
5	1 4	syl	$⊢ φ \to X \in J$
6		cnex	$⊢ ℂ \in V$
7		ssid	$⊢ X \subseteq X$
8		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
9		zsscn	$⊢ ℤ \subseteq ℂ$
10	8 9	sstri	$⊢ ℤ_{\geq M} \subseteq ℂ$
11		pmss12g	$⊢ ((X \subseteq X \land ℤ_{\geq M} \subseteq ℂ) \land (X \in J \land ℂ \in V)) \to X ↑_{𝑝𝑚} ℤ_{\geq M} \subseteq X ↑_{𝑝𝑚} ℂ$
12	7 10 11	mpanl12	$⊢ (X \in J \land ℂ \in V) \to X ↑_{𝑝𝑚} ℤ_{\geq M} \subseteq X ↑_{𝑝𝑚} ℂ$
13	5 6 12	sylancl	$⊢ φ \to X ↑_{𝑝𝑚} ℤ_{\geq M} \subseteq X ↑_{𝑝𝑚} ℂ$
14		fvex	$⊢ ℤ_{\geq M} \in V$
15		pmresg	$⊢ (ℤ_{\geq M} \in V \land F \in (X ↑_{𝑝𝑚} ℂ)) \to {F ↾}_{ℤ_{\geq M}} \in (X ↑_{𝑝𝑚} ℤ_{\geq M})$
16	14 2 15	sylancr	$⊢ φ \to {F ↾}_{ℤ_{\geq M}} \in (X ↑_{𝑝𝑚} ℤ_{\geq M})$
17	13 16	sseldd	$⊢ φ \to {F ↾}_{ℤ_{\geq M}} \in (X ↑_{𝑝𝑚} ℂ)$
18	17 2	2thd	$⊢ φ \to ({F ↾}_{ℤ_{\geq M}} \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow F \in (X ↑_{𝑝𝑚} ℂ))$
19		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
20	19	uztrn2	$⊢ (j \in ℤ_{\geq M} \land k \in ℤ_{\geq j}) \to k \in ℤ_{\geq M}$
21		dmres	$⊢ dom ({F ↾}_{ℤ_{\geq M}}) = ℤ_{\geq M} \cap dom F$
22	21	elin2	$⊢ k \in dom ({F ↾}_{ℤ_{\geq M}}) \leftrightarrow (k \in ℤ_{\geq M} \land k \in dom F)$
23	22	baib	$⊢ k \in ℤ_{\geq M} \to (k \in dom ({F ↾}_{ℤ_{\geq M}}) \leftrightarrow k \in dom F)$
24		fvres	$⊢ k \in ℤ_{\geq M} \to ({F ↾}_{ℤ_{\geq M}}) (k) = F (k)$
25	24	eleq1d	$⊢ k \in ℤ_{\geq M} \to (({F ↾}_{ℤ_{\geq M}}) (k) \in u \leftrightarrow F (k) \in u)$
26	23 25	anbi12d	$⊢ k \in ℤ_{\geq M} \to ((k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u) \leftrightarrow (k \in dom F \land F (k) \in u))$
27	20 26	syl	$⊢ (j \in ℤ_{\geq M} \land k \in ℤ_{\geq j}) \to ((k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u) \leftrightarrow (k \in dom F \land F (k) \in u))$
28	27	ralbidva	$⊢ j \in ℤ_{\geq M} \to (\forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
29	28	rexbiia	$⊢ \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u) \leftrightarrow \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
30	29	imbi2i	$⊢ (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u)) \leftrightarrow (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
31	30	ralbii	$⊢ \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u)) \leftrightarrow \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
32	31	a1i	$⊢ φ \to (\forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u)) \leftrightarrow \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
33	18 32	3anbi13d	$⊢ φ \to (({F ↾}_{ℤ_{\geq M}} \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u))) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
34	1 19 3	lmbr2	$⊢ φ \to (({F ↾}_{ℤ_{\geq M}}) \underset{t}{⇝} (J) P \leftrightarrow ({F ↾}_{ℤ_{\geq M}} \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom ({F ↾}_{ℤ_{\geq M}}) \land ({F ↾}_{ℤ_{\geq M}}) (k) \in u))))$
35	1 19 3	lmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ_{\geq M} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
36	33 34 35	3bitr4rd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow ({F ↾}_{ℤ_{\geq M}}) \underset{t}{⇝} (J) P)$

Metamath Proof Explorer

Theorem lmres

Proof