limsupequzmpt

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupequzmpt.j	$⊢ Ⅎ j φ$
	limsupequzmpt.m	$⊢ φ \to M \in ℤ$
	limsupequzmpt.n	$⊢ φ \to N \in ℤ$
	limsupequzmpt.a	$⊢ A = ℤ_{\geq M}$
	limsupequzmpt.b	$⊢ B = ℤ_{\geq N}$
	limsupequzmpt.c	$⊢ (φ \land j \in A) \to C \in V$
	limsupequzmpt.d	$⊢ (φ \land j \in B) \to C \in W$
Assertion	limsupequzmpt	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((j \in B ⟼ C))$

Step	Hyp	Ref	Expression
1		limsupequzmpt.j	$⊢ Ⅎ j φ$
2		limsupequzmpt.m	$⊢ φ \to M \in ℤ$
3		limsupequzmpt.n	$⊢ φ \to N \in ℤ$
4		limsupequzmpt.a	$⊢ A = ℤ_{\geq M}$
5		limsupequzmpt.b	$⊢ B = ℤ_{\geq N}$
6		limsupequzmpt.c	$⊢ (φ \land j \in A) \to C \in V$
7		limsupequzmpt.d	$⊢ (φ \land j \in B) \to C \in W$
8		eqid	$⊢ if (M \leq N, N, M) = if (M \leq N, N, M)$
9	1 2 3 4 5 6 7 8	limsupequzmptlem	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((j \in B ⟼ C))$

Metamath Proof Explorer