limsupmnflem

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsupmnflem.a	$⊢ φ \to A \subseteq ℝ$
2		limsupmnflem.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
3		limsupmnflem.g	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{*} <))$
4		nfv	$⊢ Ⅎ k φ$
5		reex	$⊢ ℝ \in V$
6	5	a1i	$⊢ φ \to ℝ \in V$
7	6 1	ssexd	$⊢ φ \to A \in V$
8	4 7 2 3	limsupval3	$⊢ φ \to lim sup (F) = inf (ran G ℝ^{*} <)$
9	3	rneqi	$⊢ ran G = ran (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{*} <))$
10	9	infeq1i	$⊢ inf (ran G ℝ^{} <) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{} <)) ℝ^{*} <)$
11	10	a1i	$⊢ φ \to inf (ran G ℝ^{} <) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{} <)) ℝ^{*} <)$
12	8 11	eqtrd	$⊢ φ \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{} <)) ℝ^{} <)$
13	12	eqeq1d	$⊢ φ \to (lim sup (F) = −∞ \leftrightarrow inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{} <)) ℝ^{} <) = −∞)$
14		nfv	$⊢ Ⅎ x φ$
15	2	fimassd	$⊢ φ \to F [[k, +∞)] \subseteq ℝ^{*}$
16	15	adantr	$⊢ (φ \land k \in ℝ) \to F [[k, +∞)] \subseteq ℝ^{*}$
17	16	supxrcld	$⊢ (φ \land k \in ℝ) \to sup (F [[k, +∞)] ℝ^{} <) \in ℝ^{}$
18	4 14 17	infxrunb3rnmpt	$⊢ φ \to (\forall x \in ℝ \exists k \in ℝ sup (F [[k, +∞)] ℝ^{} <) \leq x \leftrightarrow inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] ℝ^{} <)) ℝ^{*} <) = −∞)$
19	15	adantr	$⊢ (φ \land x \in ℝ) \to F [[k, +∞)] \subseteq ℝ^{*}$
20		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
21	20	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
22	21	sselda	$⊢ (φ \land x \in ℝ) \to x \in ℝ^{*}$
23		supxrleub	$⊢ (F [[k, +∞)] \subseteq ℝ^{} \land x \in ℝ^{}) \to (sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \forall y \in F [[k, +∞)] y \leq x)$
24	19 22 23	syl2anc	$⊢ (φ \land x \in ℝ) \to (sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \forall y \in F [[k, +∞)] y \leq x)$
25	24	adantr	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \forall y \in F [[k, +∞)] y \leq x)$
26	2	ffnd	$⊢ φ \to F Fn A$
27	26	ad3antrrr	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to F Fn A$
28		simplr	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j \in A$
29	20	sseli	$⊢ k \in ℝ \to k \in ℝ^{*}$
30	29	ad3antlr	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to k \in ℝ^{*}$
31		pnfxr	$⊢ +∞ \in ℝ^{*}$
32	31	a1i	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to +∞ \in ℝ^{*}$
33	20	a1i	$⊢ (φ \land j \in A) \to ℝ \subseteq ℝ^{*}$
34	1	sselda	$⊢ (φ \land j \in A) \to j \in ℝ$
35	33 34	sseldd	$⊢ (φ \land j \in A) \to j \in ℝ^{*}$
36	35	ad4ant13	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j \in ℝ^{*}$
37		simpr	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to k \leq j$
38	34	ltpnfd	$⊢ (φ \land j \in A) \to j < +∞$
39	38	ad4ant13	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j < +∞$
40	30 32 36 37 39	elicod	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to j \in [k, +∞)$
41	27 28 40	fnfvimad	$⊢ (((φ \land k \in ℝ) \land j \in A) \land k \leq j) \to F (j) \in F [[k, +∞)]$
42	41	adantllr	$⊢ ((((φ \land k \in ℝ) \land \forall y \in F [[k, +∞)] y \leq x) \land j \in A) \land k \leq j) \to F (j) \in F [[k, +∞)]$
43		simpllr	$⊢ ((((φ \land k \in ℝ) \land \forall y \in F [[k, +∞)] y \leq x) \land j \in A) \land k \leq j) \to \forall y \in F [[k, +∞)] y \leq x$
44		breq1	$⊢ y = F (j) \to (y \leq x \leftrightarrow F (j) \leq x)$
45	44	rspcva	$⊢ (F (j) \in F [[k, +∞)] \land \forall y \in F [[k, +∞)] y \leq x) \to F (j) \leq x$
46	42 43 45	syl2anc	$⊢ ((((φ \land k \in ℝ) \land \forall y \in F [[k, +∞)] y \leq x) \land j \in A) \land k \leq j) \to F (j) \leq x$
47	46	adantl4r	$⊢ (((((φ \land x \in ℝ) \land k \in ℝ) \land \forall y \in F [[k, +∞)] y \leq x) \land j \in A) \land k \leq j) \to F (j) \leq x$
48	47	ex	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land \forall y \in F [[k, +∞)] y \leq x) \land j \in A) \to (k \leq j \to F (j) \leq x)$
49	48	ralrimiva	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land \forall y \in F [[k, +∞)] y \leq x) \to \forall j \in A (k \leq j \to F (j) \leq x)$
50	49	ex	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall y \in F [[k, +∞)] y \leq x \to \forall j \in A (k \leq j \to F (j) \leq x))$
51		nfcv	$⊢ \underline{Ⅎ} j F$
52	26	adantr	$⊢ (φ \land y \in F [[k, +∞)]) \to F Fn A$
53		simpr	$⊢ (φ \land y \in F [[k, +∞)]) \to y \in F [[k, +∞)]$
54	51 52 53	fvelimad	$⊢ (φ \land y \in F [[k, +∞)]) \to \exists j \in (A \cap [k, +∞)) F (j) = y$
55	54	ad4ant14	$⊢ (((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \land y \in F [[k, +∞)]) \to \exists j \in (A \cap [k, +∞)) F (j) = y$
56		nfv	$⊢ Ⅎ j (φ \land k \in ℝ)$
57		nfra1	$⊢ Ⅎ j \forall j \in A (k \leq j \to F (j) \leq x)$
58	56 57	nfan	$⊢ Ⅎ j ((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x))$
59		nfv	$⊢ Ⅎ j y \leq x$
60	29	adantr	$⊢ (k \in ℝ \land j \in (A \cap [k, +∞))) \to k \in ℝ^{*}$
61	31	a1i	$⊢ (k \in ℝ \land j \in (A \cap [k, +∞))) \to +∞ \in ℝ^{*}$
62		elinel2	$⊢ j \in (A \cap [k, +∞)) \to j \in [k, +∞)$
63	62	adantl	$⊢ (k \in ℝ \land j \in (A \cap [k, +∞))) \to j \in [k, +∞)$
64	60 61 63	icogelbd	$⊢ (k \in ℝ \land j \in (A \cap [k, +∞))) \to k \leq j$
65	64	adantlr	$⊢ ((k \in ℝ \land \forall j \in A (k \leq j \to F (j) \leq x)) \land j \in (A \cap [k, +∞))) \to k \leq j$
66		elinel1	$⊢ j \in (A \cap [k, +∞)) \to j \in A$
67	66	adantl	$⊢ (\forall j \in A (k \leq j \to F (j) \leq x) \land j \in (A \cap [k, +∞))) \to j \in A$
68		rspa	$⊢ (\forall j \in A (k \leq j \to F (j) \leq x) \land j \in A) \to (k \leq j \to F (j) \leq x)$
69	67 68	syldan	$⊢ (\forall j \in A (k \leq j \to F (j) \leq x) \land j \in (A \cap [k, +∞))) \to (k \leq j \to F (j) \leq x)$
70	69	adantll	$⊢ ((k \in ℝ \land \forall j \in A (k \leq j \to F (j) \leq x)) \land j \in (A \cap [k, +∞))) \to (k \leq j \to F (j) \leq x)$
71	65 70	mpd	$⊢ ((k \in ℝ \land \forall j \in A (k \leq j \to F (j) \leq x)) \land j \in (A \cap [k, +∞))) \to F (j) \leq x$
72		id	$⊢ F (j) = y \to F (j) = y$
73	72	eqcomd	$⊢ F (j) = y \to y = F (j)$
74	73	adantl	$⊢ (F (j) \leq x \land F (j) = y) \to y = F (j)$
75		simpl	$⊢ (F (j) \leq x \land F (j) = y) \to F (j) \leq x$
76	74 75	eqbrtrd	$⊢ (F (j) \leq x \land F (j) = y) \to y \leq x$
77	76	ex	$⊢ F (j) \leq x \to (F (j) = y \to y \leq x)$
78	71 77	syl	$⊢ ((k \in ℝ \land \forall j \in A (k \leq j \to F (j) \leq x)) \land j \in (A \cap [k, +∞))) \to (F (j) = y \to y \leq x)$
79	78	adantlll	$⊢ (((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \land j \in (A \cap [k, +∞))) \to (F (j) = y \to y \leq x)$
80	79	ex	$⊢ ((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \to (j \in (A \cap [k, +∞)) \to (F (j) = y \to y \leq x))$
81	58 59 80	rexlimd	$⊢ ((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \to (\exists j \in (A \cap [k, +∞)) F (j) = y \to y \leq x)$
82	81	imp	$⊢ (((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \land \exists j \in (A \cap [k, +∞)) F (j) = y) \to y \leq x$
83	55 82	syldan	$⊢ (((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \land y \in F [[k, +∞)]) \to y \leq x$
84	83	ralrimiva	$⊢ ((φ \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \to \forall y \in F [[k, +∞)] y \leq x$
85	84	adantllr	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \to \forall y \in F [[k, +∞)] y \leq x$
86	24	ad2antrr	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \to (sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \forall y \in F [[k, +∞)] y \leq x)$
87	85 86	mpbird	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land \forall j \in A (k \leq j \to F (j) \leq x)) \to sup (F [[k, +∞)] ℝ^{*} <) \leq x$
88	87	ex	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall j \in A (k \leq j \to F (j) \leq x) \to sup (F [[k, +∞)] ℝ^{*} <) \leq x)$
89	88 25	sylibd	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall j \in A (k \leq j \to F (j) \leq x) \to \forall y \in F [[k, +∞)] y \leq x)$
90	50 89	impbid	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall y \in F [[k, +∞)] y \leq x \leftrightarrow \forall j \in A (k \leq j \to F (j) \leq x))$
91	25 90	bitrd	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \forall j \in A (k \leq j \to F (j) \leq x))$
92	91	rexbidva	$⊢ (φ \land x \in ℝ) \to (\exists k \in ℝ sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$
93	92	ralbidva	$⊢ φ \to (\forall x \in ℝ \exists k \in ℝ sup (F [[k, +∞)] ℝ^{*} <) \leq x \leftrightarrow \forall x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$
94	13 18 93	3bitr2d	$⊢ φ \to (lim sup (F) = −∞ \leftrightarrow \forall x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$

Metamath Proof Explorer

Theorem limsupmnflem

Proof