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 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
liminfresicompt.2 ⊢ 𝑍 = ( 𝑀 [,) +∞ )
liminfresicompt.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion liminfresicompt ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 liminfresicompt.1 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
2 liminfresicompt.2 ⊢ 𝑍 = ( 𝑀 [,) +∞ )
3 liminfresicompt.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 resmpt3 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 )
5 4 eqcomi ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 )
6 5 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) )
7 6 fveq2d ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) ) = ( lim inf ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) ) )
8 3 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
9 1 2 8 liminfresico ⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑍 ) ) = ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
10 7 9 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ ( 𝐴 ∩ 𝑍 ) ↦ 𝐵 ) ) = ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )