limsupequzmptf

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	limsupequzmptf.j	$⊢ Ⅎ j φ$
	limsupequzmptf.o	$⊢ \underline{Ⅎ} j A$
	limsupequzmptf.p	$⊢ \underline{Ⅎ} j B$
	limsupequzmptf.m	$⊢ φ \to M \in ℤ$
	limsupequzmptf.n	$⊢ φ \to N \in ℤ$
	limsupequzmptf.a	$⊢ A = ℤ_{\geq M}$
	limsupequzmptf.b	$⊢ B = ℤ_{\geq N}$
	limsupequzmptf.c	$⊢ (φ \land j \in A) \to C \in V$
	limsupequzmptf.d	$⊢ (φ \land j \in B) \to C \in W$
Assertion	limsupequzmptf	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((j \in B ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		limsupequzmptf.j	$⊢ Ⅎ j φ$
2		limsupequzmptf.o	$⊢ \underline{Ⅎ} j A$
3		limsupequzmptf.p	$⊢ \underline{Ⅎ} j B$
4		limsupequzmptf.m	$⊢ φ \to M \in ℤ$
5		limsupequzmptf.n	$⊢ φ \to N \in ℤ$
6		limsupequzmptf.a	$⊢ A = ℤ_{\geq M}$
7		limsupequzmptf.b	$⊢ B = ℤ_{\geq N}$
8		limsupequzmptf.c	$⊢ (φ \land j \in A) \to C \in V$
9		limsupequzmptf.d	$⊢ (φ \land j \in B) \to C \in W$
10		nfv	$⊢ Ⅎ k φ$
11	2	nfcri	$⊢ Ⅎ j k \in A$
12	1 11	nfan	$⊢ Ⅎ j (φ \land k \in A)$
13		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ k / j ⦌ C$
14		nfcv	$⊢ \underline{Ⅎ} j V$
15	13 14	nfel	$⊢ Ⅎ j ⦋ k / j ⦌ C \in V$
16	12 15	nfim	$⊢ Ⅎ j ((φ \land k \in A) \to ⦋ k / j ⦌ C \in V)$
17		eleq1w	$⊢ j = k \to (j \in A \leftrightarrow k \in A)$
18	17	anbi2d	$⊢ j = k \to ((φ \land j \in A) \leftrightarrow (φ \land k \in A))$
19		csbeq1a	$⊢ j = k \to C = ⦋ k / j ⦌ C$
20	19	eleq1d	$⊢ j = k \to (C \in V \leftrightarrow ⦋ k / j ⦌ C \in V)$
21	18 20	imbi12d	$⊢ j = k \to (((φ \land j \in A) \to C \in V) \leftrightarrow ((φ \land k \in A) \to ⦋ k / j ⦌ C \in V))$
22	16 21 8	chvarfv	$⊢ (φ \land k \in A) \to ⦋ k / j ⦌ C \in V$
23	3	nfcri	$⊢ Ⅎ j k \in B$
24	1 23	nfan	$⊢ Ⅎ j (φ \land k \in B)$
25		nfcv	$⊢ \underline{Ⅎ} j W$
26	13 25	nfel	$⊢ Ⅎ j ⦋ k / j ⦌ C \in W$
27	24 26	nfim	$⊢ Ⅎ j ((φ \land k \in B) \to ⦋ k / j ⦌ C \in W)$
28		eleq1w	$⊢ j = k \to (j \in B \leftrightarrow k \in B)$
29	28	anbi2d	$⊢ j = k \to ((φ \land j \in B) \leftrightarrow (φ \land k \in B))$
30	19	eleq1d	$⊢ j = k \to (C \in W \leftrightarrow ⦋ k / j ⦌ C \in W)$
31	29 30	imbi12d	$⊢ j = k \to (((φ \land j \in B) \to C \in W) \leftrightarrow ((φ \land k \in B) \to ⦋ k / j ⦌ C \in W))$
32	27 31 9	chvarfv	$⊢ (φ \land k \in B) \to ⦋ k / j ⦌ C \in W$
33	10 4 5 6 7 22 32	limsupequzmpt	$⊢ φ \to lim sup ((k \in A ⟼ ⦋ k / j ⦌ C)) = lim sup ((k \in B ⟼ ⦋ k / j ⦌ C))$
34		nfcv	$⊢ \underline{Ⅎ} k A$
35		nfcv	$⊢ \underline{Ⅎ} k C$
36	2 34 35 13 19	cbvmptf	$⊢ (j \in A ⟼ C) = (k \in A ⟼ ⦋ k / j ⦌ C)$
37	36	fveq2i	$⊢ lim sup ((j \in A ⟼ C)) = lim sup ((k \in A ⟼ ⦋ k / j ⦌ C))$
38	37	a1i	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((k \in A ⟼ ⦋ k / j ⦌ C))$
39		nfcv	$⊢ \underline{Ⅎ} k B$
40	3 39 35 13 19	cbvmptf	$⊢ (j \in B ⟼ C) = (k \in B ⟼ ⦋ k / j ⦌ C)$
41	40	fveq2i	$⊢ lim sup ((j \in B ⟼ C)) = lim sup ((k \in B ⟼ ⦋ k / j ⦌ C))$
42	41	a1i	$⊢ φ \to lim sup ((j \in B ⟼ C)) = lim sup ((k \in B ⟼ ⦋ k / j ⦌ C))$
43	33 38 42	3eqtr4d	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((j \in B ⟼ C))$

Metamath Proof Explorer

Theorem limsupequzmptf

Proof