liminfval2

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

	Ref	Expression
Hypotheses	liminfval2.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
	liminfval2.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	liminfval2.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	liminfval2.4	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) = +∞ )
Assertion	liminfval2	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		liminfval2.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
2		liminfval2.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		liminfval2.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		liminfval2.4	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) = +∞ )
5		oveq1	⊢ ( 𝑘 = 𝑗 → ( 𝑘 [,) +∞ ) = ( 𝑗 [,) +∞ ) )
6	5	imaeq2d	⊢ ( 𝑘 = 𝑗 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑗 [,) +∞ ) ) )
7	6	ineq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) )
8	7	infeq1d	⊢ ( 𝑘 = 𝑗 → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) = inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
9	8	cbvmptv	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑗 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
10	1 9	eqtri	⊢ 𝐺 = ( 𝑗 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
11	10	liminfval	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ^* , < ) )
12	2 11	syl	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ^* , < ) )
13	3	ssrexr	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
14		supxrunb1	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ^* , < ) = +∞ ) )
15	13 14	syl	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ^* , < ) = +∞ ) )
16	4 15	mpbird	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 )
17	10	liminfgf	⊢ 𝐺 : ℝ ⟶ ℝ^*
18	17	ffvelrni	⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) ∈ ℝ^* )
19	18	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ^* )
20		simpll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝜑 )
21		simprl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
22	3	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
23	17	ffvelrni	⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) ∈ ℝ^* )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ^* )
25	20 21 24	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ^* )
26		imassrn	⊢ ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺
27		frn	⊢ ( 𝐺 : ℝ ⟶ ℝ^* → ran 𝐺 ⊆ ℝ^* )
28	17 27	ax-mp	⊢ ran 𝐺 ⊆ ℝ^*
29	26 28	sstri	⊢ ( 𝐺 “ 𝐴 ) ⊆ ℝ^*
30		supxrcl	⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ℝ^* → sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* )
31	29 30	ax-mp	⊢ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^*
32	31	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* )
33		simplr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ )
34	20 21 22	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
35		simprr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
36		liminfgord	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑛 ≤ 𝑥 ) → inf ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
37	33 34 35 36	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
38	10	liminfgval	⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) = inf ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
39	38	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑛 ) = inf ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
40	10	liminfgval	⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) = inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
41	22 40	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
42	41	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
43	39 42	breq12d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ inf ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
44	43	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ inf ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ≤ inf ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
45	37 44	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑥 ) )
46	29	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 “ 𝐴 ) ⊆ ℝ^* )
47		nfv	⊢ Ⅎ 𝑗 𝜑
48		inss2	⊢ ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ⊆ ℝ^*
49		infxrcl	⊢ ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) ⊆ ℝ^* → inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ ℝ^* )
50	48 49	ax-mp	⊢ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ ℝ^*
51	50	a1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℝ ) → inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ ℝ^* )
52	47 51 10	fnmptd	⊢ ( 𝜑 → 𝐺 Fn ℝ )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐺 Fn ℝ )
54		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
55	53 22 54	fnfvimad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
56		supxrub	⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ^* ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
57	46 55 56	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
58	20 21 57	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
59	19 25 32 45 58	xrletrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
60	59	rexlimdvaa	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ) )
61	60	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → ∀ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ) )
62	16 61	mpd	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
63		xrltso	⊢ < Or ℝ^*
64	63	infex	⊢ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ V
65	64	rgenw	⊢ ∀ 𝑗 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ V
66	10	fnmpt	⊢ ( ∀ 𝑗 ∈ ℝ inf ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ∈ V → 𝐺 Fn ℝ )
67	65 66	ax-mp	⊢ 𝐺 Fn ℝ
68		breq1	⊢ ( 𝑥 = ( 𝐺 ‘ 𝑛 ) → ( 𝑥 ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ) )
69	68	ralrn	⊢ ( 𝐺 Fn ℝ → ( ∀ 𝑥 ∈ ran 𝐺 𝑥 ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ∀ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ) )
70	67 69	ax-mp	⊢ ( ∀ 𝑥 ∈ ran 𝐺 𝑥 ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ∀ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
71	62 70	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 𝑥 ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
72		supxrleub	⊢ ( ( ran 𝐺 ⊆ ℝ^* ∧ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* ) → ( sup ( ran 𝐺 , ℝ^* , < ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 𝑥 ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ) )
73	28 31 72	mp2an	⊢ ( sup ( ran 𝐺 , ℝ^* , < ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 𝑥 ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
74	71 73	sylibr	⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ^* , < ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
75	26	a1i	⊢ ( 𝜑 → ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺 )
76	28	a1i	⊢ ( 𝜑 → ran 𝐺 ⊆ ℝ^* )
77		supxrss	⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺 ∧ ran 𝐺 ⊆ ℝ^* ) → sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ sup ( ran 𝐺 , ℝ^* , < ) )
78	75 76 77	syl2anc	⊢ ( 𝜑 → sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ sup ( ran 𝐺 , ℝ^* , < ) )
79		supxrcl	⊢ ( ran 𝐺 ⊆ ℝ^* → sup ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^* )
80	28 79	ax-mp	⊢ sup ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^*
81		xrletri3	⊢ ( ( sup ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^* ∧ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* ) → ( sup ( ran 𝐺 , ℝ^* , < ) = sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ( sup ( ran 𝐺 , ℝ^* , < ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∧ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ sup ( ran 𝐺 , ℝ^* , < ) ) ) )
82	80 31 81	mp2an	⊢ ( sup ( ran 𝐺 , ℝ^* , < ) = sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ( sup ( ran 𝐺 , ℝ^* , < ) ≤ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∧ sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ sup ( ran 𝐺 , ℝ^* , < ) ) )
83	74 78 82	sylanbrc	⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ^* , < ) = sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
84	12 83	eqtrd	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem liminfval2

Proof