limsupresico

Description: The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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

Metamath Proof Explorer

Theorem limsupresico

Proof