lmcvg

Description: Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Hypotheses	lmcvg.1	$⊢ Z = ℤ_{\geq M}$
	lmcvg.3	$⊢ φ \to P \in U$
	lmcvg.4	$⊢ φ \to M \in ℤ$
	lmcvg.5	$⊢ φ \to F \underset{t}{⇝} (J) P$
	lmcvg.6	$⊢ φ \to U \in J$
Assertion	lmcvg	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in U$

Proof

Step	Hyp	Ref	Expression
1		lmcvg.1	$⊢ Z = ℤ_{\geq M}$
2		lmcvg.3	$⊢ φ \to P \in U$
3		lmcvg.4	$⊢ φ \to M \in ℤ$
4		lmcvg.5	$⊢ φ \to F \underset{t}{⇝} (J) P$
5		lmcvg.6	$⊢ φ \to U \in J$
6		eleq2	$⊢ u = U \to (P \in u \leftrightarrow P \in U)$
7		eleq2	$⊢ u = U \to (F (k) \in u \leftrightarrow F (k) \in U)$
8	7	rexralbidv	$⊢ u = U \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in U)$
9	6 8	imbi12d	$⊢ u = U \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u) \leftrightarrow (P \in U \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in U))$
10		lmrcl	$⊢ F \underset{t}{⇝} (J) P \to J \in Top$
11	4 10	syl	$⊢ φ \to J \in Top$
12		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
13	11 12	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
14	13 1 3	lmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (⋃ J ↑_{𝑝𝑚} ℂ) \land P \in ⋃ J \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
15	4 14	mpbid	$⊢ φ \to (F \in (⋃ J ↑_{𝑝𝑚} ℂ) \land P \in ⋃ J \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
16	15	simp3d	$⊢ φ \to \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
17		simpr	$⊢ (k \in dom F \land F (k) \in u) \to F (k) \in u$
18	17	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \to \forall k \in ℤ_{\geq j} F (k) \in u$
19	18	reximi	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u$
20	19	imim2i	$⊢ (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \to (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)$
21	20	ralimi	$⊢ \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \to \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)$
22	16 21	syl	$⊢ φ \to \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in u)$
23	9 22 5	rspcdva	$⊢ φ \to (P \in U \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in U)$
24	2 23	mpd	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in U$

Metamath Proof Explorer

Theorem lmcvg

Proof