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	$⊢ φ \to M \in ℝ$
		liminfresicompt.2	$⊢ Z = [M, +∞)$
		liminfresicompt.3	$⊢ φ \to A \in V$
	Assertion	liminfresicompt	$⊢ φ \to lim inf ((x \in (A \cap Z) ⟼ B)) = lim inf ((x \in A ⟼ B))$

Proof

Step	Hyp	Ref	Expression
1		liminfresicompt.1	$⊢ φ \to M \in ℝ$
2		liminfresicompt.2	$⊢ Z = [M, +∞)$
3		liminfresicompt.3	$⊢ φ \to A \in V$
4		resmpt3	$⊢ {(x \in A ⟼ B) ↾}_{Z} = (x \in (A \cap Z) ⟼ B)$
5	4	eqcomi	$⊢ (x \in (A \cap Z) ⟼ B) = {(x \in A ⟼ B) ↾}_{Z}$
6	5	a1i	$⊢ φ \to (x \in (A \cap Z) ⟼ B) = {(x \in A ⟼ B) ↾}_{Z}$
7	6	fveq2d	$⊢ φ \to lim inf ((x \in (A \cap Z) ⟼ B)) = lim inf ({(x \in A ⟼ B) ↾}_{Z})$
8	3	mptexd	$⊢ φ \to (x \in A ⟼ B) \in V$
9	1 2 8	liminfresico	$⊢ φ \to lim inf ({(x \in A ⟼ B) ↾}_{Z}) = lim inf ((x \in A ⟼ B))$
10	7 9	eqtrd	$⊢ φ \to lim inf ((x \in (A \cap Z) ⟼ B)) = lim inf ((x \in A ⟼ B))$