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 jφ
limsupequzmpt2.o _jA
limsupequzmpt2.p _jB
limsupequzmpt2.a A=M
limsupequzmpt2.b B=N
limsupequzmpt2.k φKA
limsupequzmpt2.e φKB
limsupequzmpt2.c φjKCV
Assertion limsupequzmpt2 φlim supjAC=lim supjBC

Proof

Step Hyp Ref Expression
1 limsupequzmpt2.j jφ
2 limsupequzmpt2.o _jA
3 limsupequzmpt2.p _jB
4 limsupequzmpt2.a A=M
5 limsupequzmpt2.b B=N
6 limsupequzmpt2.k φKA
7 limsupequzmpt2.e φKB
8 limsupequzmpt2.c φjKCV
9 4 6 uzssd2 φKA
10 9 adantr φjKKA
11 simpr φjKjK
12 10 11 sseldd φjKjA
13 8 elexd φjKCV
14 12 13 jca φjKjACV
15 rabid jjA|CVjACV
16 14 15 sylibr φjKjjA|CV
17 16 ex φjKjjA|CV
18 1 17 ralrimi φjKjjA|CV
19 nfcv _jK
20 nfrab1 _jjA|CV
21 19 20 dfss3f KjA|CVjKjjA|CV
22 18 21 sylibr φKjA|CV
23 20 19 resmptf KjA|CVjjA|CVCK=jKC
24 22 23 syl φjjA|CVCK=jKC
25 24 eqcomd φjKC=jjA|CVCK
26 25 fveq2d φlim supjKC=lim supjjA|CVCK
27 4 6 eluzelz2d φK
28 eqid K=K
29 4 fvexi AV
30 2 29 rabexf jA|CVV
31 20 30 mptexf jjA|CVCV
32 31 a1i φjjA|CVCV
33 eqid jjA|CVC=jjA|CVC
34 20 33 dmmptssf domjjA|CVCjA|CV
35 2 ssrab2f jA|CVA
36 uzssz M
37 4 36 eqsstri A
38 35 37 sstri jA|CV
39 34 38 sstri domjjA|CVC
40 39 a1i φdomjjA|CVC
41 27 28 32 40 limsupresuz2 φlim supjjA|CVCK=lim supjjA|CVC
42 26 41 eqtr2d φlim supjjA|CVC=lim supjKC
43 5 7 uzssd2 φKB
44 43 adantr φjKKB
45 44 11 sseldd φjKjB
46 45 13 jca φjKjBCV
47 rabid jjB|CVjBCV
48 46 47 sylibr φjKjjB|CV
49 48 ex φjKjjB|CV
50 1 49 ralrimi φjKjjB|CV
51 nfrab1 _jjB|CV
52 19 51 dfss3f KjB|CVjKjjB|CV
53 50 52 sylibr φKjB|CV
54 51 19 resmptf KjB|CVjjB|CVCK=jKC
55 53 54 syl φjjB|CVCK=jKC
56 55 eqcomd φjKC=jjB|CVCK
57 56 fveq2d φlim supjKC=lim supjjB|CVCK
58 5 fvexi BV
59 3 58 rabexf jB|CVV
60 51 59 mptexf jjB|CVCV
61 60 a1i φjjB|CVCV
62 eqid jjB|CVC=jjB|CVC
63 51 62 dmmptssf domjjB|CVCjB|CV
64 3 ssrab2f jB|CVB
65 uzssz N
66 5 65 eqsstri B
67 64 66 sstri jB|CV
68 63 67 sstri domjjB|CVC
69 68 a1i φdomjjB|CVC
70 27 28 61 69 limsupresuz2 φlim supjjB|CVCK=lim supjjB|CVC
71 57 70 eqtr2d φlim supjjB|CVC=lim supjKC
72 42 71 eqtr4d φlim supjjA|CVC=lim supjjB|CVC
73 eqid jA|CV=jA|CV
74 2 73 mptssid jAC=jjA|CVC
75 74 fveq2i lim supjAC=lim supjjA|CVC
76 75 a1i φlim supjAC=lim supjjA|CVC
77 eqid jB|CV=jB|CV
78 3 77 mptssid jBC=jjB|CVC
79 78 fveq2i lim supjBC=lim supjjB|CVC
80 79 a1i φlim supjBC=lim supjjB|CVC
81 72 76 80 3eqtr4d φlim supjAC=lim supjBC