Theorem limsupresicompt

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

	Ref	Expression
Hypotheses	limsupresicompt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	limsupresicompt.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	limsupresicompt.z	⊢ 𝑍 = ( 𝑀 [,) +∞ )
Assertion	limsupresicompt	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupresicompt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		limsupresicompt.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
3		limsupresicompt.z	⊢ 𝑍 = ( 𝑀 [,) +∞ )
4	1	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
5	2 3 4	limsupresico	⊢ ( 𝜑 → ( lim sup ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) ) = ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
6		resmpt3	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 )
7	6	a1i	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) )
8	7	fveq2d	⊢ ( 𝜑 → ( lim sup ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) ) )
9	5 8	eqtr3d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( lim sup ‘ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) ) )