This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )