Theorem liminfresicompt

Description: The inferior 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	liminfresicompt.1	|- ( ph -> M e. RR )
	liminfresicompt.2	|- Z = ( M [,) +oo )
	liminfresicompt.3	|- ( ph -> A e. V )
Assertion	liminfresicompt	|- ( ph -> ( liminf ` ( x e. ( A i^i Z ) |-> B ) ) = ( liminf ` ( x e. A |-> B ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfresicompt.1	|- ( ph -> M e. RR )
2		liminfresicompt.2	|- Z = ( M [,) +oo )
3		liminfresicompt.3	|- ( ph -> A e. V )
4		resmpt3	|- ( ( x e. A |-> B ) |` Z ) = ( x e. ( A i^i Z ) |-> B )
5	4	eqcomi	|- ( x e. ( A i^i Z ) |-> B ) = ( ( x e. A |-> B ) |` Z )
6	5	a1i	|- ( ph -> ( x e. ( A i^i Z ) |-> B ) = ( ( x e. A |-> B ) |` Z ) )
7	6	fveq2d	|- ( ph -> ( liminf ` ( x e. ( A i^i Z ) |-> B ) ) = ( liminf ` ( ( x e. A |-> B ) |` Z ) ) )
8	3	mptexd	|- ( ph -> ( x e. A |-> B ) e. _V )
9	1 2 8	liminfresico	|- ( ph -> ( liminf ` ( ( x e. A |-> B ) |` Z ) ) = ( liminf ` ( x e. A |-> B ) ) )
10	7 9	eqtrd	|- ( ph -> ( liminf ` ( x e. ( A i^i Z ) |-> B ) ) = ( liminf ` ( x e. A |-> B ) ) )