xlimmnfvlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		xlimmnfvlem1.m	$⊢ φ \to M \in ℤ$
2		xlimmnfvlem1.z	$⊢ Z = ℤ_{\geq M}$
3		xlimmnfvlem1.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		xlimmnfvlem1.c	$⊢ φ \to F \underset{*}{⇝} −∞$
5		xlimmnfvlem1.x	$⊢ φ \to X \in ℝ$
6		icomnfordt	$⊢ [−∞, 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	15	simp2d	$⊢ φ \to −∞ \in ℝ^{*}$
19	5	rexrd	$⊢ φ \to X \in ℝ^{*}$
20	5	mnfltd	$⊢ φ \to −∞ < X$
21		lbico1	$⊢ (−∞ \in ℝ^{} \land X \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	3	ffdmd	$⊢ φ \to F : dom F ⟶ ℝ^{*}$
34	33	ffvelcdmda	$⊢ (φ \land k \in dom F) \to F (k) \in ℝ^{*}$
35	34	adantrr	$⊢ (φ \land (k \in dom F \land F (k) \in [−∞, X))) \to F (k) \in ℝ^{*}$
36	19	adantr	$⊢ (φ \land (k \in dom F \land F (k) \in [−∞, X))) \to X \in ℝ^{*}$
37	18	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	37 36 38	icoltubd	$⊢ (φ \land (k \in dom F \land F (k) \in [−∞, X))) \to F (k) < X$
40	35 36 39	xrltled	$⊢ (φ \land (k \in dom F \land F (k) \in [−∞, X))) \to F (k) \leq X$
41	40	ex	$⊢ φ \to ((k \in dom F \land F (k) \in [−∞, X)) \to F (k) \leq X)$
42	41	adantr	$⊢ (φ \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in [−∞, X)) \to F (k) \leq X)$
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} F (k) \leq X)$
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} F (k) \leq X))$
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} F (k) \leq X)$
46	30 45	mpd	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) \leq X$
47	2	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq X \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) \leq X)$
48	1 47	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq X \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) \leq X)$
49	46 48	mpbird	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq X$

Metamath Proof Explorer

Theorem xlimmnfvlem1

Proof