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	|- ( ph -> A e. V )
	limsupresicompt.m	|- ( ph -> M e. RR )
	limsupresicompt.z	|- Z = ( M [,) +oo )
Assertion	limsupresicompt	|- ( ph -> ( limsup ` ( x e. A |-> B ) ) = ( limsup ` ( x e. ( A i^i Z ) |-> B ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupresicompt.a	|- ( ph -> A e. V )
2		limsupresicompt.m	|- ( ph -> M e. RR )
3		limsupresicompt.z	|- Z = ( M [,) +oo )
4	1	mptexd	|- ( ph -> ( x e. A |-> B ) e. _V )
5	2 3 4	limsupresico	|- ( ph -> ( limsup ` ( ( x e. A |-> B ) |` Z ) ) = ( limsup ` ( x e. A |-> B ) ) )
6		resmpt3	|- ( ( x e. A |-> B ) |` Z ) = ( x e. ( A i^i Z ) |-> B )
7	6	a1i	|- ( ph -> ( ( x e. A |-> B ) |` Z ) = ( x e. ( A i^i Z ) |-> B ) )
8	7	fveq2d	|- ( ph -> ( limsup ` ( ( x e. A |-> B ) |` Z ) ) = ( limsup ` ( x e. ( A i^i Z ) |-> B ) ) )
9	5 8	eqtr3d	|- ( ph -> ( limsup ` ( x e. A |-> B ) ) = ( limsup ` ( x e. ( A i^i Z ) |-> B ) ) )