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 
|- F/ j ph
limsupequzmpt2.o 
|- F/_ j A
limsupequzmpt2.p 
|- F/_ j B
limsupequzmpt2.a 
|- A = ( ZZ>= ` M )
limsupequzmpt2.b 
|- B = ( ZZ>= ` N )
limsupequzmpt2.k 
|- ( ph -> K e. A )
limsupequzmpt2.e 
|- ( ph -> K e. B )
limsupequzmpt2.c 
|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )
Assertion limsupequzmpt2 
|- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )

Proof

Step Hyp Ref Expression
1 limsupequzmpt2.j 
 |-  F/ j ph
2 limsupequzmpt2.o 
 |-  F/_ j A
3 limsupequzmpt2.p 
 |-  F/_ j B
4 limsupequzmpt2.a 
 |-  A = ( ZZ>= ` M )
5 limsupequzmpt2.b 
 |-  B = ( ZZ>= ` N )
6 limsupequzmpt2.k 
 |-  ( ph -> K e. A )
7 limsupequzmpt2.e 
 |-  ( ph -> K e. B )
8 limsupequzmpt2.c 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )
9 4 6 uzssd2 
 |-  ( ph -> ( ZZ>= ` K ) C_ A )
10 9 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` K ) C_ A )
11 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. ( ZZ>= ` K ) )
12 10 11 sseldd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. A )
13 8 elexd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. _V )
14 12 13 jca 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j e. A /\ C e. _V ) )
15 rabid 
 |-  ( j e. { j e. A | C e. _V } <-> ( j e. A /\ C e. _V ) )
16 14 15 sylibr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. { j e. A | C e. _V } )
17 16 ex 
 |-  ( ph -> ( j e. ( ZZ>= ` K ) -> j e. { j e. A | C e. _V } ) )
18 1 17 ralrimi 
 |-  ( ph -> A. j e. ( ZZ>= ` K ) j e. { j e. A | C e. _V } )
19 nfcv 
 |-  F/_ j ( ZZ>= ` K )
20 nfrab1 
 |-  F/_ j { j e. A | C e. _V }
21 19 20 dfss3f 
 |-  ( ( ZZ>= ` K ) C_ { j e. A | C e. _V } <-> A. j e. ( ZZ>= ` K ) j e. { j e. A | C e. _V } )
22 18 21 sylibr 
 |-  ( ph -> ( ZZ>= ` K ) C_ { j e. A | C e. _V } )
23 20 19 resmptf 
 |-  ( ( ZZ>= ` K ) C_ { j e. A | C e. _V } -> ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
24 22 23 syl 
 |-  ( ph -> ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
25 24 eqcomd 
 |-  ( ph -> ( j e. ( ZZ>= ` K ) |-> C ) = ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) )
26 25 fveq2d 
 |-  ( ph -> ( limsup ` ( j e. ( ZZ>= ` K ) |-> C ) ) = ( limsup ` ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) )
27 4 6 eluzelz2d 
 |-  ( ph -> K e. ZZ )
28 eqid 
 |-  ( ZZ>= ` K ) = ( ZZ>= ` K )
29 4 fvexi 
 |-  A e. _V
30 2 29 rabexf 
 |-  { j e. A | C e. _V } e. _V
31 20 30 mptexf 
 |-  ( j e. { j e. A | C e. _V } |-> C ) e. _V
32 31 a1i 
 |-  ( ph -> ( j e. { j e. A | C e. _V } |-> C ) e. _V )
33 eqid 
 |-  ( j e. { j e. A | C e. _V } |-> C ) = ( j e. { j e. A | C e. _V } |-> C )
34 20 33 dmmptssf 
 |-  dom ( j e. { j e. A | C e. _V } |-> C ) C_ { j e. A | C e. _V }
35 2 ssrab2f 
 |-  { j e. A | C e. _V } C_ A
36 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
37 4 36 eqsstri 
 |-  A C_ ZZ
38 35 37 sstri 
 |-  { j e. A | C e. _V } C_ ZZ
39 34 38 sstri 
 |-  dom ( j e. { j e. A | C e. _V } |-> C ) C_ ZZ
40 39 a1i 
 |-  ( ph -> dom ( j e. { j e. A | C e. _V } |-> C ) C_ ZZ )
41 27 28 32 40 limsupresuz2 
 |-  ( ph -> ( limsup ` ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) = ( limsup ` ( j e. { j e. A | C e. _V } |-> C ) ) )
42 26 41 eqtr2d 
 |-  ( ph -> ( limsup ` ( j e. { j e. A | C e. _V } |-> C ) ) = ( limsup ` ( j e. ( ZZ>= ` K ) |-> C ) ) )
43 5 7 uzssd2 
 |-  ( ph -> ( ZZ>= ` K ) C_ B )
44 43 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` K ) C_ B )
45 44 11 sseldd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. B )
46 45 13 jca 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j e. B /\ C e. _V ) )
47 rabid 
 |-  ( j e. { j e. B | C e. _V } <-> ( j e. B /\ C e. _V ) )
48 46 47 sylibr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. { j e. B | C e. _V } )
49 48 ex 
 |-  ( ph -> ( j e. ( ZZ>= ` K ) -> j e. { j e. B | C e. _V } ) )
50 1 49 ralrimi 
 |-  ( ph -> A. j e. ( ZZ>= ` K ) j e. { j e. B | C e. _V } )
51 nfrab1 
 |-  F/_ j { j e. B | C e. _V }
52 19 51 dfss3f 
 |-  ( ( ZZ>= ` K ) C_ { j e. B | C e. _V } <-> A. j e. ( ZZ>= ` K ) j e. { j e. B | C e. _V } )
53 50 52 sylibr 
 |-  ( ph -> ( ZZ>= ` K ) C_ { j e. B | C e. _V } )
54 51 19 resmptf 
 |-  ( ( ZZ>= ` K ) C_ { j e. B | C e. _V } -> ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
55 53 54 syl 
 |-  ( ph -> ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
56 55 eqcomd 
 |-  ( ph -> ( j e. ( ZZ>= ` K ) |-> C ) = ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) )
57 56 fveq2d 
 |-  ( ph -> ( limsup ` ( j e. ( ZZ>= ` K ) |-> C ) ) = ( limsup ` ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) )
58 5 fvexi 
 |-  B e. _V
59 3 58 rabexf 
 |-  { j e. B | C e. _V } e. _V
60 51 59 mptexf 
 |-  ( j e. { j e. B | C e. _V } |-> C ) e. _V
61 60 a1i 
 |-  ( ph -> ( j e. { j e. B | C e. _V } |-> C ) e. _V )
62 eqid 
 |-  ( j e. { j e. B | C e. _V } |-> C ) = ( j e. { j e. B | C e. _V } |-> C )
63 51 62 dmmptssf 
 |-  dom ( j e. { j e. B | C e. _V } |-> C ) C_ { j e. B | C e. _V }
64 3 ssrab2f 
 |-  { j e. B | C e. _V } C_ B
65 uzssz 
 |-  ( ZZ>= ` N ) C_ ZZ
66 5 65 eqsstri 
 |-  B C_ ZZ
67 64 66 sstri 
 |-  { j e. B | C e. _V } C_ ZZ
68 63 67 sstri 
 |-  dom ( j e. { j e. B | C e. _V } |-> C ) C_ ZZ
69 68 a1i 
 |-  ( ph -> dom ( j e. { j e. B | C e. _V } |-> C ) C_ ZZ )
70 27 28 61 69 limsupresuz2 
 |-  ( ph -> ( limsup ` ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) = ( limsup ` ( j e. { j e. B | C e. _V } |-> C ) ) )
71 57 70 eqtr2d 
 |-  ( ph -> ( limsup ` ( j e. { j e. B | C e. _V } |-> C ) ) = ( limsup ` ( j e. ( ZZ>= ` K ) |-> C ) ) )
72 42 71 eqtr4d 
 |-  ( ph -> ( limsup ` ( j e. { j e. A | C e. _V } |-> C ) ) = ( limsup ` ( j e. { j e. B | C e. _V } |-> C ) ) )
73 eqid 
 |-  { j e. A | C e. _V } = { j e. A | C e. _V }
74 2 73 mptssid 
 |-  ( j e. A |-> C ) = ( j e. { j e. A | C e. _V } |-> C )
75 74 fveq2i 
 |-  ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. { j e. A | C e. _V } |-> C ) )
76 75 a1i 
 |-  ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. { j e. A | C e. _V } |-> C ) ) )
77 eqid 
 |-  { j e. B | C e. _V } = { j e. B | C e. _V }
78 3 77 mptssid 
 |-  ( j e. B |-> C ) = ( j e. { j e. B | C e. _V } |-> C )
79 78 fveq2i 
 |-  ( limsup ` ( j e. B |-> C ) ) = ( limsup ` ( j e. { j e. B | C e. _V } |-> C ) )
80 79 a1i 
 |-  ( ph -> ( limsup ` ( j e. B |-> C ) ) = ( limsup ` ( j e. { j e. B | C e. _V } |-> C ) ) )
81 72 76 80 3eqtr4d 
 |-  ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )