liminfval2

Description: The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		liminfval2.1	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		liminfval2.2	$⊢ φ \to F \in V$
3		liminfval2.3	$⊢ φ \to A \subseteq ℝ$
4		liminfval2.4	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
5		oveq1	$⊢ k = j \to [k, +∞) = [j, +∞)$
6	5	imaeq2d	$⊢ k = j \to F [[k, +∞)] = F [[j, +∞)]$
7	6	ineq1d	$⊢ k = j \to F [[k, +∞)] \cap ℝ^{} = F [[j, +∞)] \cap ℝ^{}$
8	7	infeq1d	$⊢ k = j \to inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) = inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)$
9	8	cbvmptv	$⊢ (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (j \in ℝ ⟼ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <))$
10	1 9	eqtri	$⊢ G = (j \in ℝ ⟼ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <))$
11	10	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran G ℝ^{*} <)$
12	2 11	syl	$⊢ φ \to lim inf (F) = sup (ran G ℝ^{*} <)$
13	3	ssrexr	$⊢ φ \to A \subseteq ℝ^{*}$
14		supxrunb1	$⊢ A \subseteq ℝ^{} \to (\forall n \in ℝ \exists x \in A n \leq x \leftrightarrow sup (A ℝ^{} <) = +∞)$
15	13 14	syl	$⊢ φ \to (\forall n \in ℝ \exists x \in A n \leq x \leftrightarrow sup (A ℝ^{*} <) = +∞)$
16	4 15	mpbird	$⊢ φ \to \forall n \in ℝ \exists x \in A n \leq x$
17	10	liminfgf	$⊢ G : ℝ ⟶ ℝ^{*}$
18	17	ffvelcdmi	$⊢ n \in ℝ \to G (n) \in ℝ^{*}$
19	18	ad2antlr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (n) \in ℝ^{*}$
20		simpll	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to φ$
21		simprl	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to x \in A$
22	3	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
23	17	ffvelcdmi	$⊢ x \in ℝ \to G (x) \in ℝ^{*}$
24	22 23	syl	$⊢ (φ \land x \in A) \to G (x) \in ℝ^{*}$
25	20 21 24	syl2anc	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (x) \in ℝ^{*}$
26		imassrn	$⊢ G [A] \subseteq ran G$
27		frn	$⊢ G : ℝ ⟶ ℝ^{} \to ran G \subseteq ℝ^{}$
28	17 27	ax-mp	$⊢ ran G \subseteq ℝ^{*}$
29	26 28	sstri	$⊢ G [A] \subseteq ℝ^{*}$
30		supxrcl	$⊢ G [A] \subseteq ℝ^{} \to sup (G [A] ℝ^{} <) \in ℝ^{*}$
31	29 30	ax-mp	$⊢ sup (G [A] ℝ^{} <) \in ℝ^{}$
32	31	a1i	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to sup (G [A] ℝ^{} <) \in ℝ^{}$
33		simplr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to n \in ℝ$
34	20 21 22	syl2anc	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to x \in ℝ$
35		simprr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to n \leq x$
36		liminfgord	$⊢ (n \in ℝ \land x \in ℝ \land n \leq x) \to inf (F [[n, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
37	33 34 35 36	syl3anc	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to inf (F [[n, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
38	10	liminfgval	$⊢ n \in ℝ \to G (n) = inf (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
39	38	ad2antlr	$⊢ ((φ \land n \in ℝ) \land x \in A) \to G (n) = inf (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
40	10	liminfgval	$⊢ x \in ℝ \to G (x) = inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
41	22 40	syl	$⊢ (φ \land x \in A) \to G (x) = inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
42	41	adantlr	$⊢ ((φ \land n \in ℝ) \land x \in A) \to G (x) = inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <)$
43	39 42	breq12d	$⊢ ((φ \land n \in ℝ) \land x \in A) \to (G (n) \leq G (x) \leftrightarrow inf (F [[n, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <))$
44	43	adantrr	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to (G (n) \leq G (x) \leftrightarrow inf (F [[n, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[x, +∞)] \cap ℝ^{} ℝ^{} <))$
45	37 44	mpbird	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (n) \leq G (x)$
46	29	a1i	$⊢ (φ \land x \in A) \to G [A] \subseteq ℝ^{*}$
47		nfv	$⊢ Ⅎ j φ$
48		inss2	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
49		infxrcl	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
50	48 49	ax-mp	$⊢ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
51	50	a1i	$⊢ (φ \land j \in ℝ) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
52	47 51 10	fnmptd	$⊢ φ \to G Fn ℝ$
53	52	adantr	$⊢ (φ \land x \in A) \to G Fn ℝ$
54		simpr	$⊢ (φ \land x \in A) \to x \in A$
55	53 22 54	fnfvimad	$⊢ (φ \land x \in A) \to G (x) \in G [A]$
56		supxrub	$⊢ (G [A] \subseteq ℝ^{} \land G (x) \in G [A]) \to G (x) \leq sup (G [A] ℝ^{} <)$
57	46 55 56	syl2anc	$⊢ (φ \land x \in A) \to G (x) \leq sup (G [A] ℝ^{*} <)$
58	20 21 57	syl2anc	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (x) \leq sup (G [A] ℝ^{*} <)$
59	19 25 32 45 58	xrletrd	$⊢ ((φ \land n \in ℝ) \land (x \in A \land n \leq x)) \to G (n) \leq sup (G [A] ℝ^{*} <)$
60	59	rexlimdvaa	$⊢ (φ \land n \in ℝ) \to (\exists x \in A n \leq x \to G (n) \leq sup (G [A] ℝ^{*} <))$
61	60	ralimdva	$⊢ φ \to (\forall n \in ℝ \exists x \in A n \leq x \to \forall n \in ℝ G (n) \leq sup (G [A] ℝ^{*} <))$
62	16 61	mpd	$⊢ φ \to \forall n \in ℝ G (n) \leq sup (G [A] ℝ^{*} <)$
63		xrltso	$⊢ < Or ℝ^{*}$
64	63	infex	$⊢ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
65	64	rgenw	$⊢ \forall j \in ℝ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
66	10	fnmpt	$⊢ \forall j \in ℝ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in V \to G Fn ℝ$
67	65 66	ax-mp	$⊢ G Fn ℝ$
68		breq1	$⊢ x = G (n) \to (x \leq sup (G [A] ℝ^{} <) \leftrightarrow G (n) \leq sup (G [A] ℝ^{} <))$
69	68	ralrn	$⊢ G Fn ℝ \to (\forall x \in ran G x \leq sup (G [A] ℝ^{} <) \leftrightarrow \forall n \in ℝ G (n) \leq sup (G [A] ℝ^{} <))$
70	67 69	ax-mp	$⊢ \forall x \in ran G x \leq sup (G [A] ℝ^{} <) \leftrightarrow \forall n \in ℝ G (n) \leq sup (G [A] ℝ^{} <)$
71	62 70	sylibr	$⊢ φ \to \forall x \in ran G x \leq sup (G [A] ℝ^{*} <)$
72		supxrleub	$⊢ (ran G \subseteq ℝ^{} \land sup (G [A] ℝ^{} <) \in ℝ^{}) \to (sup (ran G ℝ^{} <) \leq sup (G [A] ℝ^{} <) \leftrightarrow \forall x \in ran G x \leq sup (G [A] ℝ^{} <))$
73	28 31 72	mp2an	$⊢ sup (ran G ℝ^{} <) \leq sup (G [A] ℝ^{} <) \leftrightarrow \forall x \in ran G x \leq sup (G [A] ℝ^{*} <)$
74	71 73	sylibr	$⊢ φ \to sup (ran G ℝ^{} <) \leq sup (G [A] ℝ^{} <)$
75	26	a1i	$⊢ φ \to G [A] \subseteq ran G$
76	28	a1i	$⊢ φ \to ran G \subseteq ℝ^{*}$
77		supxrss	$⊢ (G [A] \subseteq ran G \land ran G \subseteq ℝ^{}) \to sup (G [A] ℝ^{} <) \leq sup (ran G ℝ^{*} <)$
78	75 76 77	syl2anc	$⊢ φ \to sup (G [A] ℝ^{} <) \leq sup (ran G ℝ^{} <)$
79		supxrcl	$⊢ ran G \subseteq ℝ^{} \to sup (ran G ℝ^{} <) \in ℝ^{*}$
80	28 79	ax-mp	$⊢ sup (ran G ℝ^{} <) \in ℝ^{}$
81		xrletri3	$⊢ (sup (ran G ℝ^{} <) \in ℝ^{} \land sup (G [A] ℝ^{} <) \in ℝ^{}) \to (sup (ran G ℝ^{} <) = sup (G [A] ℝ^{} <) \leftrightarrow (sup (ran G ℝ^{} <) \leq sup (G [A] ℝ^{} <) \land sup (G [A] ℝ^{} <) \leq sup (ran G ℝ^{} <)))$
82	80 31 81	mp2an	$⊢ sup (ran G ℝ^{} <) = sup (G [A] ℝ^{} <) \leftrightarrow (sup (ran G ℝ^{} <) \leq sup (G [A] ℝ^{} <) \land sup (G [A] ℝ^{} <) \leq sup (ran G ℝ^{} <))$
83	74 78 82	sylanbrc	$⊢ φ \to sup (ran G ℝ^{} <) = sup (G [A] ℝ^{} <)$
84	12 83	eqtrd	$⊢ φ \to lim inf (F) = sup (G [A] ℝ^{*} <)$

Metamath Proof Explorer

Theorem liminfval2

Proof