Theorem dfxlim2

Description: An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	dfxlim2.k	$$⊢\underset{\_}{Ⅎ}kF$$
	dfxlim2.m	$$⊢\phi \to M\in \mathbb{Z}$$
	dfxlim2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	dfxlim2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	dfxlim2	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow \left(F⇝A\vee \left(A=\mathrm{-\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)\vee \left(A=\mathrm{+\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfxlim2.k	$$⊢\underset{\_}{Ⅎ}kF$$
2		dfxlim2.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		dfxlim2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		dfxlim2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5	2 3 4	dfxlim2v	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow \left(F⇝A\vee \left(A=\mathrm{-\infty }\wedge \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\vee \left(A=\mathrm{+\infty }\wedge \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\right)\right)\right)$$
6		biid	$$⊢F⇝A\leftrightarrow F⇝A$$
7		breq2	$$⊢y=x\to \left(F\left(l\right)\le y\leftrightarrow F\left(l\right)\le x\right)$$
8	7	rexralbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\right)$$
9		fveq2	$$⊢i=j\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge j}$$
10	9	raleqdv	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge j}F\left(l\right)\le x\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}kl$$
12	1 11	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(l\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
15	12 13 14	nfbr	$$⊢ℲkF\left(l\right)\le x$$
16		nfv	$$⊢ℲlF\left(k\right)\le x$$
17		fveq2	$$⊢l=k\to F\left(l\right)=F\left(k\right)$$
18	17	breq1d	$$⊢l=k\to \left(F\left(l\right)\le x\leftrightarrow F\left(k\right)\le x\right)$$
19	15 16 18	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge j}F\left(l\right)\le x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x$$
20	10 19	bitrdi	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)$$
21	20	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x$$
22	8 21	bitrdi	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)$$
23	22	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x$$
24	23	anbi2i	$$⊢\left(A=\mathrm{-\infty }\wedge \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\leftrightarrow \left(A=\mathrm{-\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)$$
25		breq1	$$⊢y=x\to \left(y\le F\left(l\right)\leftrightarrow x\le F\left(l\right)\right)$$
26	25	rexralbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\right)$$
27	9	raleqdv	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge j}x\le F\left(l\right)\right)$$
28	14 13 12	nfbr	$$⊢Ⅎkx\le F\left(l\right)$$
29		nfv	$$⊢Ⅎlx\le F\left(k\right)$$
30	17	breq2d	$$⊢l=k\to \left(x\le F\left(l\right)\leftrightarrow x\le F\left(k\right)\right)$$
31	28 29 30	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge j}x\le F\left(l\right)\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)$$
32	27 31	bitrdi	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)$$
33	32	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)$$
34	26 33	bitrdi	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)$$
35	34	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)$$
36	35	anbi2i	$$⊢\left(A=\mathrm{+\infty }\wedge \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\right)\leftrightarrow \left(A=\mathrm{+\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)$$
37	6 24 36	3orbi123i	$$⊢\left(F⇝A\vee \left(A=\mathrm{-\infty }\wedge \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\vee \left(A=\mathrm{+\infty }\wedge \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\right)\right)\leftrightarrow \left(F⇝A\vee \left(A=\mathrm{-\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)\vee \left(A=\mathrm{+\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)\right)$$
38	5 37	bitrdi	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow \left(F⇝A\vee \left(A=\mathrm{-\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)\vee \left(A=\mathrm{+\infty }\wedge \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)\right)\right)$$