Metamath Proof Explorer

Theorem limsupequzmptlem

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 limsupequzmptlem.j 
|- F/ j ph
limsupequzmptlem.m 
|- ( ph -> M e. ZZ )
limsupequzmptlem.n 
|- ( ph -> N e. ZZ )
limsupequzmptlem.a 
|- A = ( ZZ>= ` M )
limsupequzmptlem.b 
|- B = ( ZZ>= ` N )
limsupequzmptlem.c 
|- ( ( ph /\ j e. A ) -> C e. V )
limsupequzmptlem.d 
|- ( ( ph /\ j e. B ) -> C e. W )
limsupequzmptlem.k 
|- K = if ( M <_ N , N , M )
Assertion limsupequzmptlem 
|- ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )

Proof

Step Hyp Ref Expression
1 limsupequzmptlem.j 
 |-  F/ j ph
2 limsupequzmptlem.m 
 |-  ( ph -> M e. ZZ )
3 limsupequzmptlem.n 
 |-  ( ph -> N e. ZZ )
4 limsupequzmptlem.a 
 |-  A = ( ZZ>= ` M )
5 limsupequzmptlem.b 
 |-  B = ( ZZ>= ` N )
6 limsupequzmptlem.c 
 |-  ( ( ph /\ j e. A ) -> C e. V )
7 limsupequzmptlem.d 
 |-  ( ( ph /\ j e. B ) -> C e. W )
8 limsupequzmptlem.k 
 |-  K = if ( M <_ N , N , M )
9 nfmpt1 
 |-  F/_ j ( j e. A |-> C )
10 nfmpt1 
 |-  F/_ j ( j e. B |-> C )
11 4 eqcomi 
 |-  ( ZZ>= ` M ) = A
12 11 eleq2i 
 |-  ( j e. ( ZZ>= ` M ) <-> j e. A )
13 12 biimpi 
 |-  ( j e. ( ZZ>= ` M ) -> j e. A )
14 13 6 sylan2 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> C e. V )
15 4 mpteq1i 
 |-  ( j e. A |-> C ) = ( j e. ( ZZ>= ` M ) |-> C )
16 1 14 15 fnmptd 
 |-  ( ph -> ( j e. A |-> C ) Fn ( ZZ>= ` M ) )
17 5 eleq2i 
 |-  ( j e. B <-> j e. ( ZZ>= ` N ) )
18 17 bicomi 
 |-  ( j e. ( ZZ>= ` N ) <-> j e. B )
19 18 biimpi 
 |-  ( j e. ( ZZ>= ` N ) -> j e. B )
20 19 7 sylan2 
 |-  ( ( ph /\ j e. ( ZZ>= ` N ) ) -> C e. W )
21 5 mpteq1i 
 |-  ( j e. B |-> C ) = ( j e. ( ZZ>= ` N ) |-> C )
22 1 20 21 fnmptd 
 |-  ( ph -> ( j e. B |-> C ) Fn ( ZZ>= ` N ) )
23 3 2 ifcld 
 |-  ( ph -> if ( M <_ N , N , M ) e. ZZ )
24 8 23 eqeltrid 
 |-  ( ph -> K e. ZZ )
25 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
26 2 zred 
 |-  ( ph -> M e. RR )
27 3 zred 
 |-  ( ph -> N e. RR )
28 max1 
 |-  ( ( M e. RR /\ N e. RR ) -> M <_ if ( M <_ N , N , M ) )
29 26 27 28 syl2anc 
 |-  ( ph -> M <_ if ( M <_ N , N , M ) )
30 29 8 breqtrrdi 
 |-  ( ph -> M <_ K )
31 25 2 24 30 eluzd 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
32 31 uzssd 
 |-  ( ph -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
33 11 a1i 
 |-  ( ph -> ( ZZ>= ` M ) = A )
34 32 33 sseqtrd 
 |-  ( ph -> ( ZZ>= ` K ) C_ A )
35 34 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` K ) C_ A )
36 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. ( ZZ>= ` K ) )
37 35 36 sseldd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. A )
38 37 6 syldan 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )
39 eqid 
 |-  ( j e. A |-> C ) = ( j e. A |-> C )
40 39 fvmpt2 
 |-  ( ( j e. A /\ C e. V ) -> ( ( j e. A |-> C ) ` j ) = C )
41 37 38 40 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( j e. A |-> C ) ` j ) = C )
42 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
43 max2 
 |-  ( ( M e. RR /\ N e. RR ) -> N <_ if ( M <_ N , N , M ) )
44 26 27 43 syl2anc 
 |-  ( ph -> N <_ if ( M <_ N , N , M ) )
45 44 8 breqtrrdi 
 |-  ( ph -> N <_ K )
46 42 3 24 45 eluzd 
 |-  ( ph -> K e. ( ZZ>= ` N ) )
47 46 uzssd 
 |-  ( ph -> ( ZZ>= ` K ) C_ ( ZZ>= ` N ) )
48 5 eqcomi 
 |-  ( ZZ>= ` N ) = B
49 48 a1i 
 |-  ( ph -> ( ZZ>= ` N ) = B )
50 47 49 sseqtrd 
 |-  ( ph -> ( ZZ>= ` K ) C_ B )
51 50 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` K ) C_ B )
52 51 36 sseldd 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. B )
53 eqid 
 |-  ( j e. B |-> C ) = ( j e. B |-> C )
54 53 fvmpt2 
 |-  ( ( j e. B /\ C e. V ) -> ( ( j e. B |-> C ) ` j ) = C )
55 52 38 54 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( j e. B |-> C ) ` j ) = C )
56 41 55 eqtr4d 
 |-  ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ( j e. A |-> C ) ` j ) = ( ( j e. B |-> C ) ` j ) )
57 1 9 10 2 16 3 22 24 56 limsupequz 
 |-  ( ph -> ( limsup ` ( j e. A |-> C ) ) = ( limsup ` ( j e. B |-> C ) ) )