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

Metamath Proof Explorer

Theorem limsupequzmpt2

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 limsupequzmpt2.j ⊢ Ⅎ 𝑗 𝜑
limsupequzmpt2.o ⊢ Ⅎ 𝑗 𝐴
limsupequzmpt2.p ⊢ Ⅎ 𝑗 𝐵
limsupequzmpt2.a ⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
limsupequzmpt2.b ⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
limsupequzmpt2.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
limsupequzmpt2.e ⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
limsupequzmpt2.c ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
Assertion limsupequzmpt2 ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 limsupequzmpt2.j ⊢ Ⅎ 𝑗 𝜑
2 limsupequzmpt2.o ⊢ Ⅎ 𝑗 𝐴
3 limsupequzmpt2.p ⊢ Ⅎ 𝑗 𝐵
4 limsupequzmpt2.a ⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
5 limsupequzmpt2.b ⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
6 limsupequzmpt2.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
7 limsupequzmpt2.e ⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
8 limsupequzmpt2.c ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
9 4 6 uzssd2 ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐴 )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐴 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) )
12 10 11 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐴 )
13 8 elexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ V )
14 12 13 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 ∈ 𝐴 ∧ 𝐶 ∈ V ) )
15 rabid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↔ ( 𝑗 ∈ 𝐴 ∧ 𝐶 ∈ V ) )
16 14 15 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
17 16 ex ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ) )
18 1 17 ralrimi ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
19 nfcv ⊢ Ⅎ 𝑗 ( ℤ≥ ‘ 𝐾 )
20 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V }
21 19 20 dfss3f ⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
22 18 21 sylibr ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
23 20 19 resmptf ⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
24 22 23 syl ⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
25 24 eqcomd ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) = ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) )
26 25 fveq2d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) = ( lim sup ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) )
27 4 6 eluzelz2d ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
28 eqid ⊢ ( ℤ≥ ‘ 𝐾 ) = ( ℤ≥ ‘ 𝐾 )
29 4 fvexi ⊢ 𝐴 ∈ V
30 2 29 rabexf ⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ∈ V
31 20 30 mptexf ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V
32 31 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V )
33 eqid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 )
34 20 33 dmmptssf ⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V }
35 2 ssrab2f ⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ⊆ 𝐴
36 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
37 4 36 eqsstri ⊢ 𝐴 ⊆ ℤ
38 35 37 sstri ⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ⊆ ℤ
39 34 38 sstri ⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ
40 39 a1i ⊢ ( 𝜑 → dom ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ )
41 27 28 32 40 limsupresuz2 ⊢ ( 𝜑 → ( lim sup ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
42 26 41 eqtr2d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) )
43 5 7 uzssd2 ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐵 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐵 )
45 44 11 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐵 )
46 45 13 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 ∈ 𝐵 ∧ 𝐶 ∈ V ) )
47 rabid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↔ ( 𝑗 ∈ 𝐵 ∧ 𝐶 ∈ V ) )
48 46 47 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
49 48 ex ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ) )
50 1 49 ralrimi ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
51 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V }
52 19 51 dfss3f ⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
53 50 52 sylibr ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
54 51 19 resmptf ⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
55 53 54 syl ⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
56 55 eqcomd ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) = ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) )
57 56 fveq2d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) = ( lim sup ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) )
58 5 fvexi ⊢ 𝐵 ∈ V
59 3 58 rabexf ⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ∈ V
60 51 59 mptexf ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V
61 60 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V )
62 eqid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 )
63 51 62 dmmptssf ⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V }
64 3 ssrab2f ⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ⊆ 𝐵
65 uzssz ⊢ ( ℤ≥ ‘ 𝑁 ) ⊆ ℤ
66 5 65 eqsstri ⊢ 𝐵 ⊆ ℤ
67 64 66 sstri ⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ⊆ ℤ
68 63 67 sstri ⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ
69 68 a1i ⊢ ( 𝜑 → dom ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ )
70 27 28 61 69 limsupresuz2 ⊢ ( 𝜑 → ( lim sup ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
71 57 70 eqtr2d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) )
72 42 71 eqtr4d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
73 eqid ⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } = { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V }
74 2 73 mptssid ⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 )
75 74 fveq2i ⊢ ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) )
76 75 a1i ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
77 eqid ⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } = { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V }
78 3 77 mptssid ⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 )
79 78 fveq2i ⊢ ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) )
80 79 a1i ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
81 72 76 80 3eqtr4d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )