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 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )