Metamath Proof Explorer

Theorem limsupresicompt

Description: The superior 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	limsupresicompt.a	$⊢ φ \to A \in V$
		limsupresicompt.m	$⊢ φ \to M \in ℝ$
		limsupresicompt.z	$⊢ Z = [M, +∞)$
	Assertion	limsupresicompt	$⊢ φ \to lim sup ((x \in A ⟼ B)) = lim sup ((x \in (A \cap Z) ⟼ B))$

Proof

Step	Hyp	Ref	Expression
1		limsupresicompt.a	$⊢ φ \to A \in V$
2		limsupresicompt.m	$⊢ φ \to M \in ℝ$
3		limsupresicompt.z	$⊢ Z = [M, +∞)$
4	1	mptexd	$⊢ φ \to (x \in A ⟼ B) \in V$
5	2 3 4	limsupresico	$⊢ φ \to lim sup ({(x \in A ⟼ B) ↾}_{Z}) = lim sup ((x \in A ⟼ B))$
6		resmpt3	$⊢ {(x \in A ⟼ B) ↾}_{Z} = (x \in (A \cap Z) ⟼ B)$
7	6	a1i	$⊢ φ \to {(x \in A ⟼ B) ↾}_{Z} = (x \in (A \cap Z) ⟼ B)$
8	7	fveq2d	$⊢ φ \to lim sup ({(x \in A ⟼ B) ↾}_{Z}) = lim sup ((x \in (A \cap Z) ⟼ B))$
9	5 8	eqtr3d	$⊢ φ \to lim sup ((x \in A ⟼ B)) = lim sup ((x \in (A \cap Z) ⟼ B))$