xlimpnfvlem1

Description: Lemma for xlimpnfv : the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimpnfvlem1.m	$⊢ φ \to M \in ℤ$
	xlimpnfvlem1.z	$⊢ Z = ℤ_{\geq M}$
	xlimpnfvlem1.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	xlimpnfvlem1.c	$⊢ φ \to F \underset{*}{⇝} +∞$
	xlimpnfvlem1.x	$⊢ φ \to X \in ℝ$
Assertion	xlimpnfvlem1	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} X \leq F (k)$

Proof

Step	Hyp	Ref	Expression
1		xlimpnfvlem1.m	$⊢ φ \to M \in ℤ$
2		xlimpnfvlem1.z	$⊢ Z = ℤ_{\geq M}$
3		xlimpnfvlem1.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		xlimpnfvlem1.c	$⊢ φ \to F \underset{*}{⇝} +∞$
5		xlimpnfvlem1.x	$⊢ φ \to X \in ℝ$
6		iocpnfordt	$⊢ (X, +∞] \in ordTop (\leq)$
7	6	a1i	$⊢ φ \to (X, +∞] \in ordTop (\leq)$
8		df-xlim	$⊢ \underset{*}{⇝} = \underset{t}{⇝} (ordTop (\leq))$
9	8	breqi	$⊢ F \underset{*}{⇝} +∞ \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) +∞$
10	4 9	sylib	$⊢ φ \to F \underset{t}{⇝} (ordTop (\leq)) +∞$
11		nfcv	$⊢ \underline{Ⅎ} k F$
12		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
13	12	a1i	$⊢ φ \to ordTop (\leq) \in TopOn (ℝ^{*})$
14	11 13	lmbr3	$⊢ φ \to (F \underset{t}{⇝} (ordTop (\leq)) +∞ \leftrightarrow (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land +∞ \in ℝ^{} \land \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
15	10 14	mpbid	$⊢ φ \to (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land +∞ \in ℝ^{} \land \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
16	15	simp3d	$⊢ φ \to \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
17	7 16	jca	$⊢ φ \to ((X, +∞] \in ordTop (\leq) \land \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
18	5	rexrd	$⊢ φ \to X \in ℝ^{*}$
19	15	simp2d	$⊢ φ \to +∞ \in ℝ^{*}$
20	5	ltpnfd	$⊢ φ \to X < +∞$
21		ubioc1	$⊢ (X \in ℝ^{} \land +∞ \in ℝ^{} \land X < +∞) \to +∞ \in (X, +∞]$
22	18 19 20 21	syl3anc	$⊢ φ \to +∞ \in (X, +∞]$
23		eleq2	$⊢ u = (X, +∞] \to (+∞ \in u \leftrightarrow +∞ \in (X, +∞])$
24		eleq2	$⊢ u = (X, +∞] \to (F (k) \in u \leftrightarrow F (k) \in (X, +∞])$
25	24	anbi2d	$⊢ u = (X, +∞] \to ((k \in dom F \land F (k) \in u) \leftrightarrow (k \in dom F \land F (k) \in (X, +∞]))$
26	25	ralbidv	$⊢ u = (X, +∞] \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞]))$
27	26	rexbidv	$⊢ u = (X, +∞] \to (\exists j \in ℤ \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 (X, +∞]))$
28	23 27	imbi12d	$⊢ u = (X, +∞] \to ((+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow (+∞ \in (X, +∞] \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞])))$
29	28	rspcva	$⊢ ((X, +∞] \in ordTop (\leq) \land \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))) \to (+∞ \in (X, +∞] \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞]))$
30	17 22 29	sylc	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞])$
31		nfv	$⊢ Ⅎ j φ$
32		nfv	$⊢ Ⅎ k φ$
33	18	adantr	$⊢ (φ \land (k \in dom F \land F (k) \in (X, +∞])) \to X \in ℝ^{*}$
34	3	ffdmd	$⊢ φ \to F : dom F ⟶ ℝ^{*}$
35	34	ffvelcdmda	$⊢ (φ \land k \in dom F) \to F (k) \in ℝ^{*}$
36	35	adantrr	$⊢ (φ \land (k \in dom F \land F (k) \in (X, +∞])) \to F (k) \in ℝ^{*}$
37	19	adantr	$⊢ (φ \land (k \in dom F \land F (k) \in (X, +∞])) \to +∞ \in ℝ^{*}$
38		simprr	$⊢ (φ \land (k \in dom F \land F (k) \in (X, +∞])) \to F (k) \in (X, +∞]$
39	33 37 38	iocgtlbd	$⊢ (φ \land (k \in dom F \land F (k) \in (X, +∞])) \to X < F (k)$
40	33 36 39	xrltled	$⊢ (φ \land (k \in dom F \land F (k) \in (X, +∞])) \to X \leq F (k)$
41	40	ex	$⊢ φ \to ((k \in dom F \land F (k) \in (X, +∞]) \to X \leq F (k))$
42	41	adantr	$⊢ (φ \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in (X, +∞]) \to X \leq F (k))$
43	32 42	ralimdaa	$⊢ φ \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞]) \to \forall k \in ℤ_{\geq j} X \leq F (k))$
44	43	a1d	$⊢ φ \to (j \in ℤ \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞]) \to \forall k \in ℤ_{\geq j} X \leq F (k)))$
45	31 44	reximdai	$⊢ φ \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (X, +∞]) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} X \leq F (k))$
46	30 45	mpd	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} X \leq F (k)$
47	2	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} X \leq F (k) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} X \leq F (k))$
48	1 47	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} X \leq F (k) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} X \leq F (k))$
49	46 48	mpbird	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} X \leq F (k)$

Metamath Proof Explorer

Theorem xlimpnfvlem1

Proof