xlimmnfvlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		xlimmnfvlem2.k	$⊢ Ⅎ k φ$
2		xlimmnfvlem2.j	$⊢ Ⅎ j φ$
3		xlimmnfvlem2.m	$⊢ φ \to M \in ℤ$
4		xlimmnfvlem2.z	$⊢ Z = ℤ_{\geq M}$
5		xlimmnfvlem2.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
6		xlimmnfvlem2.g	$⊢ φ \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) < x$
7		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
8	7	a1i	$⊢ φ \to ordTop (\leq) \in TopOn (ℝ^{*})$
9	8	elfvexd	$⊢ φ \to ℝ^{*} \in V$
10		cnex	$⊢ ℂ \in V$
11	10	a1i	$⊢ φ \to ℂ \in V$
12	4	uzsscn2	$⊢ Z \subseteq ℂ$
13	12	a1i	$⊢ φ \to Z \subseteq ℂ$
14		elpm2r	$⊢ ((ℝ^{} \in V \land ℂ \in V) \land (F : Z ⟶ ℝ^{} \land Z \subseteq ℂ)) \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
15	9 11 5 13 14	syl22anc	$⊢ φ \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
16		mnfxr	$⊢ −∞ \in ℝ^{*}$
17	16	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
18		mnfnei	$⊢ (u \in ordTop (\leq) \land −∞ \in u) \to \exists x \in ℝ [−∞, x) \subseteq u$
19	18	adantll	$⊢ ((φ \land u \in ordTop (\leq)) \land −∞ \in u) \to \exists x \in ℝ [−∞, x) \subseteq u$
20		nfv	$⊢ Ⅎ j x \in ℝ$
21	2 20	nfan	$⊢ Ⅎ j (φ \land x \in ℝ)$
22		nfv	$⊢ Ⅎ j [−∞, x) \subseteq u$
23	21 22	nfan	$⊢ Ⅎ j ((φ \land x \in ℝ) \land [−∞, x) \subseteq u)$
24		simprr	$⊢ (((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) < x)) \to \forall k \in ℤ_{\geq j} F (k) < x$
25		nfv	$⊢ Ⅎ k x \in ℝ$
26	1 25	nfan	$⊢ Ⅎ k (φ \land x \in ℝ)$
27		nfv	$⊢ Ⅎ k [−∞, x) \subseteq u$
28	26 27	nfan	$⊢ Ⅎ k ((φ \land x \in ℝ) \land [−∞, x) \subseteq u)$
29		nfv	$⊢ Ⅎ k j \in Z$
30	28 29	nfan	$⊢ Ⅎ k (((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z)$
31	4	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
32	31	3adant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
33	5	fdmd	$⊢ φ \to dom F = Z$
34	33	3ad2ant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to dom F = Z$
35	32 34	eleqtrrd	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to k \in dom F$
36	35	ad5ant134	$⊢ ((((φ \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to k \in dom F$
37	36	adantl4r	$⊢ (((((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to k \in dom F$
38		simp-4r	$⊢ ((((φ \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to [−∞, x) \subseteq u$
39	38	adantl4r	$⊢ (((((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to [−∞, x) \subseteq u$
40	16	a1i	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to −∞ \in ℝ^{*}$
41		simp-4r	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to x \in ℝ$
42		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
43	41 42	syl	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to x \in ℝ^{*}$
44		simp-4l	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to φ$
45	31	ad4ant23	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to k \in Z$
46	5	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ^{*}$
47	44 45 46	syl2anc	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to F (k) \in ℝ^{*}$
48	47	mnfled	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to −∞ \leq F (k)$
49		simpr	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to F (k) < x$
50	40 43 47 48 49	elicod	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to F (k) \in [−∞, x)$
51	50	adantl3r	$⊢ (((((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to F (k) \in [−∞, x)$
52	39 51	sseldd	$⊢ (((((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to F (k) \in u$
53	37 52	jca	$⊢ (((((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) < x) \to (k \in dom F \land F (k) \in u)$
54	53	ex	$⊢ ((((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) < x \to (k \in dom F \land F (k) \in u))$
55	30 54	ralimda	$⊢ (((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z) \to (\forall k \in ℤ_{\geq j} F (k) < x \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
56	55	adantrr	$⊢ (((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) < x)) \to (\forall k \in ℤ_{\geq j} F (k) < x \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
57	24 56	mpd	$⊢ (((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) < x)) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
58	57	3impb	$⊢ (((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \land j \in Z \land \forall k \in ℤ_{\geq j} F (k) < x) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
59	6	r19.21bi	$⊢ (φ \land x \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) < x$
60	59	adantr	$⊢ ((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) < x$
61	23 58 60	reximdd	$⊢ ((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
62	4	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))$
63	3 62	syl	$⊢ φ \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))$
64	63	ad2antrr	$⊢ ((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \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))$
65	61 64	mpbid	$⊢ ((φ \land x \in ℝ) \land [−∞, x) \subseteq u) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
66	65	rexlimdva2	$⊢ φ \to (\exists x \in ℝ [−∞, x) \subseteq u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
67	66	ad2antrr	$⊢ ((φ \land u \in ordTop (\leq)) \land −∞ \in u) \to (\exists x \in ℝ [−∞, x) \subseteq u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
68	19 67	mpd	$⊢ ((φ \land u \in ordTop (\leq)) \land −∞ \in u) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
69	68	ex	$⊢ (φ \land u \in ordTop (\leq)) \to (−∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
70	69	ralrimiva	$⊢ φ \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))$
71	15 17 70	3jca	$⊢ φ \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)))$
72		nfcv	$⊢ \underline{Ⅎ} k F$
73	72 8	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))))$
74	71 73	mpbird	$⊢ φ \to F \underset{t}{⇝} (ordTop (\leq)) −∞$
75		df-xlim	$⊢ \underset{*}{⇝} = \underset{t}{⇝} (ordTop (\leq))$
76	75	breqi	$⊢ F \underset{*}{⇝} −∞ \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) −∞$
77	76	a1i	$⊢ φ \to (F \underset{*}{⇝} −∞ \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) −∞)$
78	74 77	mpbird	$⊢ φ \to F \underset{*}{⇝} −∞$

Metamath Proof Explorer

Theorem xlimmnfvlem2

Proof