Metamath Proof Explorer


Theorem liminfequzmpt2

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfequzmpt2.j
|- F/ j ph
liminfequzmpt2.o
|- F/_ j A
liminfequzmpt2.p
|- F/_ j B
liminfequzmpt2.a
|- A = ( ZZ>= ` M )
liminfequzmpt2.b
|- B = ( ZZ>= ` N )
liminfequzmpt2.k
|- ( ph -> K e. A )
liminfequzmpt2.e
|- ( ph -> K e. B )
liminfequzmpt2.c
|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )
Assertion liminfequzmpt2
|- ( ph -> ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. B |-> C ) ) )

Proof

Step Hyp Ref Expression
1 liminfequzmpt2.j
 |-  F/ j ph
2 liminfequzmpt2.o
 |-  F/_ j A
3 liminfequzmpt2.p
 |-  F/_ j B
4 liminfequzmpt2.a
 |-  A = ( ZZ>= ` M )
5 liminfequzmpt2.b
 |-  B = ( ZZ>= ` N )
6 liminfequzmpt2.k
 |-  ( ph -> K e. A )
7 liminfequzmpt2.e
 |-  ( ph -> K e. B )
8 liminfequzmpt2.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 -> ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) = ( liminf ` ( ( 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 liminfresuz2
 |-  ( ph -> ( liminf ` ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) = ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) )
42 26 41 eqtr2d
 |-  ( ph -> ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) = ( liminf ` ( 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 -> ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) = ( liminf ` ( ( 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 liminfresuz2
 |-  ( ph -> ( liminf ` ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) )
71 57 70 eqtr2d
 |-  ( ph -> ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) = ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) )
72 42 71 eqtr4d
 |-  ( ph -> ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) = ( liminf ` ( 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
 |-  ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) )
76 75 a1i
 |-  ( ph -> ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( 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
 |-  ( liminf ` ( j e. B |-> C ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) )
80 79 a1i
 |-  ( ph -> ( liminf ` ( j e. B |-> C ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) )
81 72 76 80 3eqtr4d
 |-  ( ph -> ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. B |-> C ) ) )