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 𝑗 𝜑
liminfequzmpt2.o 𝑗 𝐴
liminfequzmpt2.p 𝑗 𝐵
liminfequzmpt2.a 𝐴 = ( ℤ𝑀 )
liminfequzmpt2.b 𝐵 = ( ℤ𝑁 )
liminfequzmpt2.k ( 𝜑𝐾𝐴 )
liminfequzmpt2.e ( 𝜑𝐾𝐵 )
liminfequzmpt2.c ( ( 𝜑𝑗 ∈ ( ℤ𝐾 ) ) → 𝐶𝑉 )
Assertion liminfequzmpt2 ( 𝜑 → ( lim inf ‘ ( 𝑗𝐴𝐶 ) ) = ( lim inf ‘ ( 𝑗𝐵𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 liminfequzmpt2.j 𝑗 𝜑
2 liminfequzmpt2.o 𝑗 𝐴
3 liminfequzmpt2.p 𝑗 𝐵
4 liminfequzmpt2.a 𝐴 = ( ℤ𝑀 )
5 liminfequzmpt2.b 𝐵 = ( ℤ𝑁 )
6 liminfequzmpt2.k ( 𝜑𝐾𝐴 )
7 liminfequzmpt2.e ( 𝜑𝐾𝐵 )
8 liminfequzmpt2.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 inf ‘ ( 𝑗 ∈ ( ℤ𝐾 ) ↦ 𝐶 ) ) = ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ 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 liminfresuz2 ( 𝜑 → ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ𝐾 ) ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 ) ) )
42 26 41 eqtr2d ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ ( ℤ𝐾 ) ↦ 𝐶 ) ) )
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 inf ‘ ( 𝑗 ∈ ( ℤ𝐾 ) ↦ 𝐶 ) ) = ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ 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 liminfresuz2 ( 𝜑 → ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ𝐾 ) ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 ) ) )
71 57 70 eqtr2d ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ ( ℤ𝐾 ) ↦ 𝐶 ) ) )
72 42 71 eqtr4d ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 ) ) )
73 eqid { 𝑗𝐴𝐶 ∈ V } = { 𝑗𝐴𝐶 ∈ V }
74 2 73 mptssid ( 𝑗𝐴𝐶 ) = ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 )
75 74 fveq2i ( lim inf ‘ ( 𝑗𝐴𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 ) )
76 75 a1i ( 𝜑 → ( lim inf ‘ ( 𝑗𝐴𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐴𝐶 ∈ V } ↦ 𝐶 ) ) )
77 eqid { 𝑗𝐵𝐶 ∈ V } = { 𝑗𝐵𝐶 ∈ V }
78 3 77 mptssid ( 𝑗𝐵𝐶 ) = ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 )
79 78 fveq2i ( lim inf ‘ ( 𝑗𝐵𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 ) )
80 79 a1i ( 𝜑 → ( lim inf ‘ ( 𝑗𝐵𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗𝐵𝐶 ∈ V } ↦ 𝐶 ) ) )
81 72 76 80 3eqtr4d ( 𝜑 → ( lim inf ‘ ( 𝑗𝐴𝐶 ) ) = ( lim inf ‘ ( 𝑗𝐵𝐶 ) ) )