limsuppnfdlem

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsuppnfdlem.a	$⊢ φ \to A \subseteq ℝ$
	limsuppnfdlem.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
	limsuppnfdlem.u	$⊢ φ \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
	limsuppnfdlem.g	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
Assertion	limsuppnfdlem	$⊢ φ \to lim sup (F) = +∞$

Proof

Step	Hyp	Ref	Expression
1		limsuppnfdlem.a	$⊢ φ \to A \subseteq ℝ$
2		limsuppnfdlem.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
3		limsuppnfdlem.u	$⊢ φ \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
4		limsuppnfdlem.g	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
5		reex	$⊢ ℝ \in V$
6	5	a1i	$⊢ φ \to ℝ \in V$
7	6 1	ssexd	$⊢ φ \to A \in V$
8	2 7	fexd	$⊢ φ \to F \in V$
9	4	limsupval	$⊢ F \in V \to lim sup (F) = sup (ran G ℝ^{*} <)$
10	8 9	syl	$⊢ φ \to lim sup (F) = sup (ran G ℝ^{*} <)$
11	2	ffund	$⊢ φ \to Fun F$
12	11	adantr	$⊢ (φ \land j \in A) \to Fun F$
13		simpr	$⊢ (φ \land j \in A) \to j \in A$
14	2	fdmd	$⊢ φ \to dom F = A$
15	14	adantr	$⊢ (φ \land j \in A) \to dom F = A$
16	13 15	eleqtrrd	$⊢ (φ \land j \in A) \to j \in dom F$
17	12 16	jca	$⊢ (φ \land j \in A) \to (Fun F \land j \in dom F)$
18	17	ad4ant13	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to (Fun F \land j \in dom F)$
19		simpllr	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to k \in ℝ$
20	19	rexrd	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to k \in ℝ^{*}$
21		pnfxr	$⊢ +∞ \in ℝ^{*}$
22	21	a1i	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to +∞ \in ℝ^{*}$
23	1	ssrexr	$⊢ φ \to A \subseteq ℝ^{*}$
24	23	sselda	$⊢ (φ \land j \in A) \to j \in ℝ^{*}$
25	24	ad4ant13	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j \in ℝ^{*}$
26		simpr	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to k \leq j$
27	1	sselda	$⊢ (φ \land j \in A) \to j \in ℝ$
28	27	ltpnfd	$⊢ (φ \land j \in A) \to j < +∞$
29	28	ad4ant13	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j < +∞$
30	20 22 25 26 29	elicod	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j \in [k, +∞)$
31		funfvima	$⊢ (Fun F \land j \in dom F) \to (j \in [k, +∞) \to F (j) \in F [[k, +∞)])$
32	18 30 31	sylc	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to F (j) \in F [[k, +∞)]$
33	2	ffvelrnda	$⊢ (φ \land j \in A) \to F (j) \in ℝ^{*}$
34	33	ad4ant13	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to F (j) \in ℝ^{*}$
35	32 34	elind	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to F (j) \in (F [[k, +∞)] \cap ℝ^{*})$
36	35	adantllr	$⊢ ((((φ \land k \in ℝ) \land x \in ℝ) \land j \in A) \land k \leq j) \to F (j) \in (F [[k, +∞)] \cap ℝ^{*})$
37	36	adantrr	$⊢ ((((φ \land k \in ℝ) \land x \in ℝ) \land j \in A) \land (k \leq j \land x \leq F (j))) \to F (j) \in (F [[k, +∞)] \cap ℝ^{*})$
38		simprr	$⊢ ((((φ \land k \in ℝ) \land x \in ℝ) \land j \in A) \land (k \leq j \land x \leq F (j))) \to x \leq F (j)$
39		breq2	$⊢ y = F (j) \to (x \leq y \leftrightarrow x \leq F (j))$
40	39	rspcev	$⊢ (F (j) \in (F [[k, +∞)] \cap ℝ^{}) \land x \leq F (j)) \to \exists y \in (F [[k, +∞)] \cap ℝ^{}) x \leq y$
41	37 38 40	syl2anc	$⊢ ((((φ \land k \in ℝ) \land x \in ℝ) \land j \in A) \land (k \leq j \land x \leq F (j))) \to \exists y \in (F [[k, +∞)] \cap ℝ^{*}) x \leq y$
42	3	r19.21bi	$⊢ (φ \land x \in ℝ) \to \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
43	42	r19.21bi	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to \exists j \in A (k \leq j \land x \leq F (j))$
44	43	an32s	$⊢ ((φ \land k \in ℝ) \land x \in ℝ) \to \exists j \in A (k \leq j \land x \leq F (j))$
45	41 44	r19.29a	$⊢ ((φ \land k \in ℝ) \land x \in ℝ) \to \exists y \in (F [[k, +∞)] \cap ℝ^{*}) x \leq y$
46	45	ralrimiva	$⊢ (φ \land k \in ℝ) \to \forall x \in ℝ \exists y \in (F [[k, +∞)] \cap ℝ^{*}) x \leq y$
47		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
48		supxrunb3	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in (F [[k, +∞)] \cap ℝ^{}) x \leq y \leftrightarrow sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <) = +∞)$
49	47 48	mp1i	$⊢ (φ \land k \in ℝ) \to (\forall x \in ℝ \exists y \in (F [[k, +∞)] \cap ℝ^{}) x \leq y \leftrightarrow sup (F [[k, +∞)] \cap ℝ^{} ℝ^{*} <) = +∞)$
50	46 49	mpbid	$⊢ (φ \land k \in ℝ) \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = +∞$
51	50	mpteq2dva	$⊢ φ \to (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ +∞)$
52	4 51	syl5eq	$⊢ φ \to G = (k \in ℝ ⟼ +∞)$
53	52	rneqd	$⊢ φ \to ran G = ran (k \in ℝ ⟼ +∞)$
54		eqid	$⊢ (k \in ℝ ⟼ +∞) = (k \in ℝ ⟼ +∞)$
55		ren0	$⊢ ℝ \neq \emptyset$
56	55	a1i	$⊢ φ \to ℝ \neq \emptyset$
57	54 56	rnmptc	$⊢ φ \to ran (k \in ℝ ⟼ +∞) = \{+∞\}$
58	53 57	eqtrd	$⊢ φ \to ran G = \{+∞\}$
59	58	infeq1d	$⊢ φ \to sup (ran G ℝ^{} <) = sup (\{+∞\} ℝ^{} <)$
60		xrltso	$⊢ < Or ℝ^{*}$
61		infsn	$⊢ (< Or ℝ^{} \land +∞ \in ℝ^{}) \to sup (\{+∞\} ℝ^{*} <) = +∞$
62	60 21 61	mp2an	$⊢ sup (\{+∞\} ℝ^{*} <) = +∞$
63	62	a1i	$⊢ φ \to sup (\{+∞\} ℝ^{*} <) = +∞$
64	10 59 63	3eqtrd	$⊢ φ \to lim sup (F) = +∞$

Metamath Proof Explorer

Theorem limsuppnfdlem

Proof