liminfresico

Description: The inferior limit doesn't change when a function is restricted to an upperset of reals. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfresico.1	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	liminfresico.2	⊢ 𝑍 = ( 𝑀 [,) +∞ )
	liminfresico.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	liminfresico	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim inf ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		liminfresico.1	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
2		liminfresico.2	⊢ 𝑍 = ( 𝑀 [,) +∞ )
3		liminfresico.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4	1	rexrd	⊢ ( 𝜑 → 𝑀 ∈ ℝ^* )
5	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑀 ∈ ℝ^* )
6		pnfxr	⊢ +∞ ∈ ℝ^*
7	6	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → +∞ ∈ ℝ^* )
8		ressxr	⊢ ℝ ⊆ ℝ^*
9	6	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
10		icossre	⊢ ( ( 𝑀 ∈ ℝ ∧ +∞ ∈ ℝ^* ) → ( 𝑀 [,) +∞ ) ⊆ ℝ )
11	1 9 10	syl2anc	⊢ ( 𝜑 → ( 𝑀 [,) +∞ ) ⊆ ℝ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑀 [,) +∞ ) ⊆ ℝ )
13	2	eleq2i	⊢ ( 𝑘 ∈ 𝑍 ↔ 𝑘 ∈ ( 𝑀 [,) +∞ ) )
14	13	bilani	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( 𝑀 [,) +∞ ) )
15	12 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℝ )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑘 ∈ ℝ )
17		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ( 𝑘 [,) +∞ ) )
18		elicore	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ℝ )
19	16 17 18	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ℝ )
20	8 19	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ℝ^* )
21	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑀 ∈ ℝ )
22	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑀 ∈ ℝ^* )
23	6	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → +∞ ∈ ℝ^* )
24	22 23 14	icogelbd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑀 ≤ 𝑘 )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑀 ≤ 𝑘 )
26	8 16	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑘 ∈ ℝ^* )
27	26 7 17	icogelbd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑘 ≤ 𝑦 )
28	21 16 19 25 27	letrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑀 ≤ 𝑦 )
29	19	ltpnfd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 < +∞ )
30	5 7 20 28 29	elicod	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ( 𝑀 [,) +∞ ) )
31	30 2	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ 𝑍 )
32	31	ssd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 [,) +∞ ) ⊆ 𝑍 )
33		resima2	⊢ ( ( 𝑘 [,) +∞ ) ⊆ 𝑍 → ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
34	32 33	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
35	34	ineq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) )
36	35	infeq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
37	36	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
38	37	rneqd	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑍 ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ran ( 𝑘 ∈ 𝑍 ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
39	2 11	eqsstrid	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
40	39	mptimass	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) = ran ( 𝑘 ∈ 𝑍 ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
41	39	mptimass	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) = ran ( 𝑘 ∈ 𝑍 ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
42	38 40 41	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) = ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) )
43	42	supeq1d	⊢ ( 𝜑 → sup ( ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) , ℝ^* , < ) = sup ( ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) , ℝ^* , < ) )
44		eqid	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
45	3	resexd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑍 ) ∈ V )
46	2	supeq1i	⊢ sup ( 𝑍 , ℝ^* , < ) = sup ( ( 𝑀 [,) +∞ ) , ℝ^* , < )
47	46	a1i	⊢ ( 𝜑 → sup ( 𝑍 , ℝ^* , < ) = sup ( ( 𝑀 [,) +∞ ) , ℝ^* , < ) )
48	1	renepnfd	⊢ ( 𝜑 → 𝑀 ≠ +∞ )
49		icopnfsup	⊢ ( ( 𝑀 ∈ ℝ^* ∧ 𝑀 ≠ +∞ ) → sup ( ( 𝑀 [,) +∞ ) , ℝ^* , < ) = +∞ )
50	4 48 49	syl2anc	⊢ ( 𝜑 → sup ( ( 𝑀 [,) +∞ ) , ℝ^* , < ) = +∞ )
51	47 50	eqtrd	⊢ ( 𝜑 → sup ( 𝑍 , ℝ^* , < ) = +∞ )
52	44 45 39 51	liminfval2	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = sup ( ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝑍 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) , ℝ^* , < ) )
53		eqid	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
54	53 3 39 51	liminfval2	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ( ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) “ 𝑍 ) , ℝ^* , < ) )
55	43 52 54	3eqtr4d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim inf ‘ 𝐹 ) )

Metamath Proof Explorer

Theorem liminfresico

Proof