This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )