limsupre2mpt

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupre2mpt.p	$⊢ Ⅎ x φ$
	limsupre2mpt.a	$⊢ φ \to A \subseteq ℝ$
	limsupre2mpt.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
Assertion	limsupre2mpt	$⊢ φ \to (lim sup ((x \in A ⟼ B)) \in ℝ \leftrightarrow (\exists y \in ℝ \forall k \in ℝ \exists x \in A (k \leq x \land y < B) \land \exists y \in ℝ \exists k \in ℝ \forall x \in A (k \leq x \to B < y)))$

Proof

Step	Hyp	Ref	Expression
1		limsupre2mpt.p	$⊢ Ⅎ x φ$
2		limsupre2mpt.a	$⊢ φ \to A \subseteq ℝ$
3		limsupre2mpt.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
4		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
5	1 3	fmptd2f	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℝ^{*}$
6	4 2 5	limsupre2	$⊢ φ \to (lim sup ((x \in A ⟼ B)) \in ℝ \leftrightarrow (\exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < (x \in A ⟼ B) (x)) \land \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to (x \in A ⟼ B) (x) < w)))$
7		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
8	7	a1i	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
9	8 3	fvmpt2d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
10	9	breq2d	$⊢ (φ \land x \in A) \to (w < (x \in A ⟼ B) (x) \leftrightarrow w < B)$
11	10	anbi2d	$⊢ (φ \land x \in A) \to ((j \leq x \land w < (x \in A ⟼ B) (x)) \leftrightarrow (j \leq x \land w < B))$
12	1 11	rexbida	$⊢ φ \to (\exists x \in A (j \leq x \land w < (x \in A ⟼ B) (x)) \leftrightarrow \exists x \in A (j \leq x \land w < B))$
13	12	ralbidv	$⊢ φ \to (\forall j \in ℝ \exists x \in A (j \leq x \land w < (x \in A ⟼ B) (x)) \leftrightarrow \forall j \in ℝ \exists x \in A (j \leq x \land w < B))$
14	13	rexbidv	$⊢ φ \to (\exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < (x \in A ⟼ B) (x)) \leftrightarrow \exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < B))$
15	9	breq1d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ B) (x) < w \leftrightarrow B < w)$
16	15	imbi2d	$⊢ (φ \land x \in A) \to ((j \leq x \to (x \in A ⟼ B) (x) < w) \leftrightarrow (j \leq x \to B < w))$
17	1 16	ralbida	$⊢ φ \to (\forall x \in A (j \leq x \to (x \in A ⟼ B) (x) < w) \leftrightarrow \forall x \in A (j \leq x \to B < w))$
18	17	rexbidv	$⊢ φ \to (\exists j \in ℝ \forall x \in A (j \leq x \to (x \in A ⟼ B) (x) < w) \leftrightarrow \exists j \in ℝ \forall x \in A (j \leq x \to B < w))$
19	18	rexbidv	$⊢ φ \to (\exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to (x \in A ⟼ B) (x) < w) \leftrightarrow \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to B < w))$
20	14 19	anbi12d	$⊢ φ \to ((\exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < (x \in A ⟼ B) (x)) \land \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to (x \in A ⟼ B) (x) < w)) \leftrightarrow (\exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < B) \land \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to B < w)))$
21		breq1	$⊢ w = y \to (w < B \leftrightarrow y < B)$
22	21	anbi2d	$⊢ w = y \to ((j \leq x \land w < B) \leftrightarrow (j \leq x \land y < B))$
23	22	rexbidv	$⊢ w = y \to (\exists x \in A (j \leq x \land w < B) \leftrightarrow \exists x \in A (j \leq x \land y < B))$
24	23	ralbidv	$⊢ w = y \to (\forall j \in ℝ \exists x \in A (j \leq x \land w < B) \leftrightarrow \forall j \in ℝ \exists x \in A (j \leq x \land y < B))$
25		breq1	$⊢ j = k \to (j \leq x \leftrightarrow k \leq x)$
26	25	anbi1d	$⊢ j = k \to ((j \leq x \land y < B) \leftrightarrow (k \leq x \land y < B))$
27	26	rexbidv	$⊢ j = k \to (\exists x \in A (j \leq x \land y < B) \leftrightarrow \exists x \in A (k \leq x \land y < B))$
28	27	cbvralvw	$⊢ \forall j \in ℝ \exists x \in A (j \leq x \land y < B) \leftrightarrow \forall k \in ℝ \exists x \in A (k \leq x \land y < B)$
29	28	a1i	$⊢ w = y \to (\forall j \in ℝ \exists x \in A (j \leq x \land y < B) \leftrightarrow \forall k \in ℝ \exists x \in A (k \leq x \land y < B))$
30	24 29	bitrd	$⊢ w = y \to (\forall j \in ℝ \exists x \in A (j \leq x \land w < B) \leftrightarrow \forall k \in ℝ \exists x \in A (k \leq x \land y < B))$
31	30	cbvrexvw	$⊢ \exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < B) \leftrightarrow \exists y \in ℝ \forall k \in ℝ \exists x \in A (k \leq x \land y < B)$
32		breq2	$⊢ w = y \to (B < w \leftrightarrow B < y)$
33	32	imbi2d	$⊢ w = y \to ((j \leq x \to B < w) \leftrightarrow (j \leq x \to B < y))$
34	33	ralbidv	$⊢ w = y \to (\forall x \in A (j \leq x \to B < w) \leftrightarrow \forall x \in A (j \leq x \to B < y))$
35	34	rexbidv	$⊢ w = y \to (\exists j \in ℝ \forall x \in A (j \leq x \to B < w) \leftrightarrow \exists j \in ℝ \forall x \in A (j \leq x \to B < y))$
36	25	imbi1d	$⊢ j = k \to ((j \leq x \to B < y) \leftrightarrow (k \leq x \to B < y))$
37	36	ralbidv	$⊢ j = k \to (\forall x \in A (j \leq x \to B < y) \leftrightarrow \forall x \in A (k \leq x \to B < y))$
38	37	cbvrexvw	$⊢ \exists j \in ℝ \forall x \in A (j \leq x \to B < y) \leftrightarrow \exists k \in ℝ \forall x \in A (k \leq x \to B < y)$
39	38	a1i	$⊢ w = y \to (\exists j \in ℝ \forall x \in A (j \leq x \to B < y) \leftrightarrow \exists k \in ℝ \forall x \in A (k \leq x \to B < y))$
40	35 39	bitrd	$⊢ w = y \to (\exists j \in ℝ \forall x \in A (j \leq x \to B < w) \leftrightarrow \exists k \in ℝ \forall x \in A (k \leq x \to B < y))$
41	40	cbvrexvw	$⊢ \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to B < w) \leftrightarrow \exists y \in ℝ \exists k \in ℝ \forall x \in A (k \leq x \to B < y)$
42	31 41	anbi12i	$⊢ (\exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < B) \land \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to B < w)) \leftrightarrow (\exists y \in ℝ \forall k \in ℝ \exists x \in A (k \leq x \land y < B) \land \exists y \in ℝ \exists k \in ℝ \forall x \in A (k \leq x \to B < y))$
43	42	a1i	$⊢ φ \to ((\exists w \in ℝ \forall j \in ℝ \exists x \in A (j \leq x \land w < B) \land \exists w \in ℝ \exists j \in ℝ \forall x \in A (j \leq x \to B < w)) \leftrightarrow (\exists y \in ℝ \forall k \in ℝ \exists x \in A (k \leq x \land y < B) \land \exists y \in ℝ \exists k \in ℝ \forall x \in A (k \leq x \to B < y)))$
44	6 20 43	3bitrd	$⊢ φ \to (lim sup ((x \in A ⟼ B)) \in ℝ \leftrightarrow (\exists y \in ℝ \forall k \in ℝ \exists x \in A (k \leq x \land y < B) \land \exists y \in ℝ \exists k \in ℝ \forall x \in A (k \leq x \to B < y)))$

Metamath Proof Explorer

Theorem limsupre2mpt

Proof