limsupval2

Description: The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	limsupval2.1	$⊢ φ \to F \in V$
	limsupval2.2	$⊢ φ \to A \subseteq ℝ$
	limsupval2.3	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
Assertion	limsupval2	$⊢ φ \to lim sup (F) = inf (G [A] ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		limsupval2.1	$⊢ φ \to F \in V$
3		limsupval2.2	$⊢ φ \to A \subseteq ℝ$
4		limsupval2.3	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
5	1	limsupval	$⊢ F \in V \to lim sup (F) = inf (ran G ℝ^{*} <)$
6	2 5	syl	$⊢ φ \to lim sup (F) = inf (ran G ℝ^{*} <)$
7		imassrn	$⊢ G [A] \subseteq ran G$
8	1	limsupgf	$⊢ G : ℝ ⟶ ℝ^{*}$
9		frn	$⊢ G : ℝ ⟶ ℝ^{} \to ran G \subseteq ℝ^{}$
10	8 9	ax-mp	$⊢ ran G \subseteq ℝ^{*}$
11		infxrlb	$⊢ (ran G \subseteq ℝ^{} \land x \in ran G) \to inf (ran G ℝ^{} <) \leq x$
12	11	ralrimiva	$⊢ ran G \subseteq ℝ^{} \to \forall x \in ran G inf (ran G ℝ^{} <) \leq x$
13	10 12	mp1i	$⊢ φ \to \forall x \in ran G inf (ran G ℝ^{*} <) \leq x$
14		ssralv	$⊢ G [A] \subseteq ran G \to (\forall x \in ran G inf (ran G ℝ^{} <) \leq x \to \forall x \in G [A] inf (ran G ℝ^{} <) \leq x)$
15	7 13 14	mpsyl	$⊢ φ \to \forall x \in G [A] inf (ran G ℝ^{*} <) \leq x$
16	7 10	sstri	$⊢ G [A] \subseteq ℝ^{*}$
17		infxrcl	$⊢ ran G \subseteq ℝ^{} \to inf (ran G ℝ^{} <) \in ℝ^{*}$
18	10 17	ax-mp	$⊢ inf (ran G ℝ^{} <) \in ℝ^{}$
19		infxrgelb	$⊢ (G [A] \subseteq ℝ^{} \land inf (ran G ℝ^{} <) \in ℝ^{}) \to (inf (ran G ℝ^{} <) \leq inf (G [A] ℝ^{} <) \leftrightarrow \forall x \in G [A] inf (ran G ℝ^{} <) \leq x)$
20	16 18 19	mp2an	$⊢ inf (ran G ℝ^{} <) \leq inf (G [A] ℝ^{} <) \leftrightarrow \forall x \in G [A] inf (ran G ℝ^{*} <) \leq x$
21	15 20	sylibr	$⊢ φ \to inf (ran G ℝ^{} <) \leq inf (G [A] ℝ^{} <)$
22		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
23	3 22	sstrdi	$⊢ φ \to A \subseteq ℝ^{*}$
24		supxrunb1	$⊢ A \subseteq ℝ^{} \to (\forall n \in ℝ \exists x \in A n \leq x \leftrightarrow sup (A ℝ^{} <) = +∞)$
25	23 24	syl	$⊢ φ \to (\forall n \in ℝ \exists x \in A n \leq x \leftrightarrow sup (A ℝ^{*} <) = +∞)$
26	4 25	mpbird	$⊢ φ \to \forall n \in ℝ \exists x \in A n \leq x$
27		infxrcl	$⊢ G [A] \subseteq ℝ^{} \to inf (G [A] ℝ^{} <) \in ℝ^{*}$
28	16 27	mp1i	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to inf (G [A] ℝ^{} <) \in ℝ^{}$
29	3	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
30	29	ad2ant2r	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to x \in ℝ$
31	8	ffvelcdmi	$⊢ x \in ℝ \to G (x) \in ℝ^{*}$
32	30 31	syl	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (x) \in ℝ^{*}$
33	8	ffvelcdmi	$⊢ n \in ℝ \to G (n) \in ℝ^{*}$
34	33	ad2antlr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (n) \in ℝ^{*}$
35		ffn	$⊢ G : ℝ ⟶ ℝ^{*} \to G Fn ℝ$
36	8 35	mp1i	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G Fn ℝ$
37	3	ad2antrr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to A \subseteq ℝ$
38		simprl	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to x \in A$
39		fnfvima	$⊢ (G Fn ℝ \land A \subseteq ℝ \land x \in A) \to G (x) \in G [A]$
40	36 37 38 39	syl3anc	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (x) \in G [A]$
41		infxrlb	$⊢ (G [A] \subseteq ℝ^{} \land G (x) \in G [A]) \to inf (G [A] ℝ^{} <) \leq G (x)$
42	16 40 41	sylancr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to inf (G [A] ℝ^{*} <) \leq G (x)$
43		simplr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to n \in ℝ$
44		simprr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to n \leq x$
45		limsupgord	$⊢ (n \in ℝ \land x \in ℝ \land n \leq x) \to sup (F [[x, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
46	43 30 44 45	syl3anc	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to sup (F [[x, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
47	1	limsupgval	$⊢ x \in ℝ \to G (x) = sup (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
48	30 47	syl	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (x) = sup (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
49	1	limsupgval	$⊢ n \in ℝ \to G (n) = sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
50	49	ad2antlr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (n) = sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
51	46 48 50	3brtr4d	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (x) \leq G (n)$
52	28 32 34 42 51	xrletrd	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to inf (G [A] ℝ^{*} <) \leq G (n)$
53	52	rexlimdvaa	$⊢ (φ \land n \in ℝ) \to (\exists x \in A n \leq x \to inf (G [A] ℝ^{*} <) \leq G (n))$
54	53	ralimdva	$⊢ φ \to (\forall n \in ℝ \exists x \in A n \leq x \to \forall n \in ℝ inf (G [A] ℝ^{*} <) \leq G (n))$
55	26 54	mpd	$⊢ φ \to \forall n \in ℝ inf (G [A] ℝ^{*} <) \leq G (n)$
56	8 35	ax-mp	$⊢ G Fn ℝ$
57		breq2	$⊢ x = G (n) \to (inf (G [A] ℝ^{} <) \leq x \leftrightarrow inf (G [A] ℝ^{} <) \leq G (n))$
58	57	ralrn	$⊢ G Fn ℝ \to (\forall x \in ran G inf (G [A] ℝ^{} <) \leq x \leftrightarrow \forall n \in ℝ inf (G [A] ℝ^{} <) \leq G (n))$
59	56 58	ax-mp	$⊢ \forall x \in ran G inf (G [A] ℝ^{} <) \leq x \leftrightarrow \forall n \in ℝ inf (G [A] ℝ^{} <) \leq G (n)$
60	55 59	sylibr	$⊢ φ \to \forall x \in ran G inf (G [A] ℝ^{*} <) \leq x$
61	16 27	ax-mp	$⊢ inf (G [A] ℝ^{} <) \in ℝ^{}$
62		infxrgelb	$⊢ (ran G \subseteq ℝ^{} \land inf (G [A] ℝ^{} <) \in ℝ^{}) \to (inf (G [A] ℝ^{} <) \leq inf (ran G ℝ^{} <) \leftrightarrow \forall x \in ran G inf (G [A] ℝ^{} <) \leq x)$
63	10 61 62	mp2an	$⊢ inf (G [A] ℝ^{} <) \leq inf (ran G ℝ^{} <) \leftrightarrow \forall x \in ran G inf (G [A] ℝ^{*} <) \leq x$
64	60 63	sylibr	$⊢ φ \to inf (G [A] ℝ^{} <) \leq inf (ran G ℝ^{} <)$
65		xrletri3	$⊢ (inf (ran G ℝ^{} <) \in ℝ^{} \land inf (G [A] ℝ^{} <) \in ℝ^{}) \to (inf (ran G ℝ^{} <) = inf (G [A] ℝ^{} <) \leftrightarrow (inf (ran G ℝ^{} <) \leq inf (G [A] ℝ^{} <) \land inf (G [A] ℝ^{} <) \leq inf (ran G ℝ^{} <)))$
66	18 61 65	mp2an	$⊢ inf (ran G ℝ^{} <) = inf (G [A] ℝ^{} <) \leftrightarrow (inf (ran G ℝ^{} <) \leq inf (G [A] ℝ^{} <) \land inf (G [A] ℝ^{} <) \leq inf (ran G ℝ^{} <))$
67	21 64 66	sylanbrc	$⊢ φ \to inf (ran G ℝ^{} <) = inf (G [A] ℝ^{} <)$
68	6 67	eqtrd	$⊢ φ \to lim sup (F) = inf (G [A] ℝ^{*} <)$

Metamath Proof Explorer

Theorem limsupval2

Proof