xlimbr

Description: Express the binary relation "sequence F converges to point P " w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimbr.k	$⊢ \underline{Ⅎ} k F$
	xlimbr.m	$⊢ φ \to M \in ℤ$
	xlimbr.z	$⊢ Z = ℤ_{\geq M}$
	xlimbr.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	xlimbr.j	$⊢ J = ordTop (\leq)$
Assertion	xlimbr	$⊢ φ \to (F \underset{}{⇝} P \leftrightarrow (P \in ℝ^{} \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))))$

Proof

Step	Hyp	Ref	Expression
1		xlimbr.k	$⊢ \underline{Ⅎ} k F$
2		xlimbr.m	$⊢ φ \to M \in ℤ$
3		xlimbr.z	$⊢ Z = ℤ_{\geq M}$
4		xlimbr.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
5		xlimbr.j	$⊢ J = ordTop (\leq)$
6		df-xlim	$⊢ \underset{*}{⇝} = \underset{t}{⇝} (ordTop (\leq))$
7	6	breqi	$⊢ F \underset{*}{⇝} P \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) P$
8	7	a1i	$⊢ φ \to (F \underset{*}{⇝} P \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) P)$
9		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
10	9	a1i	$⊢ φ \to ordTop (\leq) \in TopOn (ℝ^{*})$
11	1 10	lmbr3	$⊢ φ \to (F \underset{t}{⇝} (ordTop (\leq)) P \leftrightarrow (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land P \in ℝ^{} \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
12		simpr2	$⊢ (φ \land (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land P \in ℝ^{} \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))) \to P \in ℝ^{*}$
13	5	eqcomi	$⊢ ordTop (\leq) = J$
14	13	raleqi	$⊢ \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
15	3	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
16	15	bicomd	$⊢ M \in ℤ \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
17	16	imbi2d	$⊢ M \in ℤ \to ((P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
18	17	biimpd	$⊢ M \in ℤ \to ((P \in u \to \exists j \in ℤ \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} (k \in dom F \land F (k) \in u)))$
19	18	ralimdv	$⊢ M \in ℤ \to (\forall u \in J (P \in u \to \exists j \in ℤ \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} (k \in dom F \land F (k) \in u)))$
20	2 19	syl	$⊢ φ \to (\forall u \in J (P \in u \to \exists j \in ℤ \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} (k \in dom F \land F (k) \in u)))$
21	20	imp	$⊢ (φ \land \forall u \in J (P \in u \to \exists j \in ℤ \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} (k \in dom F \land F (k) \in u))$
22	14 21	sylan2b	$⊢ (φ \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \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} (k \in dom F \land F (k) \in u))$
23	22	3ad2antr3	$⊢ (φ \land (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land P \in ℝ^{} \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \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} (k \in dom F \land F (k) \in u))$
24	12 23	jca	$⊢ (φ \land (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land P \in ℝ^{} \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))) \to (P \in ℝ^{*} \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)))$
25		cnex	$⊢ ℂ \in V$
26	25	a1i	$⊢ φ \to ℂ \in V$
27	10	elfvexd	$⊢ φ \to ℝ^{*} \in V$
28	3	uzsscn2	$⊢ Z \subseteq ℂ$
29	28	a1i	$⊢ φ \to Z \subseteq ℂ$
30	26 27 29 4	fpmd	$⊢ φ \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
31	30	adantr	$⊢ (φ \land (P \in ℝ^{} \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)))) \to F \in (ℝ^{} ↑_{𝑝𝑚} ℂ)$
32		simprl	$⊢ (φ \land (P \in ℝ^{} \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)))) \to P \in ℝ^{}$
33	17	biimprd	$⊢ M \in ℤ \to ((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 ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
34	33	ralimdv	$⊢ M \in ℤ \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)) \to \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
35	2 34	syl	$⊢ φ \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)) \to \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
36	35	imp	$⊢ (φ \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))) \to \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
37	5	raleqi	$⊢ \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
38	36 37	sylib	$⊢ (φ \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))) \to \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
39	38	adantrl	$⊢ (φ \land (P \in ℝ^{*} \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)))) \to \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
40	31 32 39	3jca	$⊢ (φ \land (P \in ℝ^{} \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)))) \to (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land P \in ℝ^{*} \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
41	24 40	impbida	$⊢ φ \to ((F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land P \in ℝ^{} \land \forall u \in ordTop (\leq) (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))) \leftrightarrow (P \in ℝ^{*} \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))))$
42	8 11 41	3bitrd	$⊢ φ \to (F \underset{}{⇝} P \leftrightarrow (P \in ℝ^{} \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))))$

Metamath Proof Explorer

Theorem xlimbr

Proof