Theorem 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	⊢ Ⅎ 𝑗 𝜑
	limsupequzmptf.o	⊢ Ⅎ 𝑗 𝐴
	limsupequzmptf.p	⊢ Ⅎ 𝑗 𝐵
	limsupequzmptf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupequzmptf.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	limsupequzmptf.a	⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
	limsupequzmptf.b	⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
	limsupequzmptf.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	limsupequzmptf.d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
Assertion	limsupequzmptf	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupequzmptf.j	⊢ Ⅎ 𝑗 𝜑
2		limsupequzmptf.o	⊢ Ⅎ 𝑗 𝐴
3		limsupequzmptf.p	⊢ Ⅎ 𝑗 𝐵
4		limsupequzmptf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		limsupequzmptf.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6		limsupequzmptf.a	⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
7		limsupequzmptf.b	⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
8		limsupequzmptf.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
9		limsupequzmptf.d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
10		nfv	⊢ Ⅎ 𝑘 𝜑
11	2	nfcri	⊢ Ⅎ 𝑗 𝑘 ∈ 𝐴
12	1 11	nfan	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ 𝐴 )
13		nfcsb1v	⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐶
14		nfcv	⊢ Ⅎ 𝑗 𝑉
15	13 14	nfel	⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑉
16	12 15	nfim	⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑉 )
17		eleq1w	⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
18	17	anbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ) )
19		csbeq1a	⊢ ( 𝑗 = 𝑘 → 𝐶 = ⦋ 𝑘 / 𝑗 ⦌ 𝐶 )
20	19	eleq1d	⊢ ( 𝑗 = 𝑘 → ( 𝐶 ∈ 𝑉 ↔ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑉 ) )
21	18 20	imbi12d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑉 ) ) )
22	16 21 8	chvarfv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑉 )
23	3	nfcri	⊢ Ⅎ 𝑗 𝑘 ∈ 𝐵
24	1 23	nfan	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ 𝐵 )
25		nfcv	⊢ Ⅎ 𝑗 𝑊
26	13 25	nfel	⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑊
27	24 26	nfim	⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑊 )
28		eleq1w	⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝐵 ↔ 𝑘 ∈ 𝐵 ) )
29	28	anbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ) )
30	19	eleq1d	⊢ ( 𝑗 = 𝑘 → ( 𝐶 ∈ 𝑊 ↔ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑊 ) )
31	29 30	imbi12d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑊 ) ) )
32	27 31 9	chvarfv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ∈ 𝑊 )
33	10 4 5 6 7 22 32	limsupequzmpt	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝐴 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ) ) = ( lim sup ‘ ( 𝑘 ∈ 𝐵 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ) ) )
34		nfcv	⊢ Ⅎ 𝑘 𝐴
35		nfcv	⊢ Ⅎ 𝑘 𝐶
36	2 34 35 13 19	cbvmptf	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 )
37	36	fveq2i	⊢ ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑘 ∈ 𝐴 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ) )
38	37	a1i	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑘 ∈ 𝐴 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ) ) )
39		nfcv	⊢ Ⅎ 𝑘 𝐵
40	3 39 35 13 19	cbvmptf	⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 )
41	40	fveq2i	⊢ ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑘 ∈ 𝐵 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ) )
42	41	a1i	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑘 ∈ 𝐵 ↦ ⦋ 𝑘 / 𝑗 ⦌ 𝐶 ) ) )
43	33 38 42	3eqtr4d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )