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 j φ
liminfequzmpt2.o _ j A
liminfequzmpt2.p _ j B
liminfequzmpt2.a A = M
liminfequzmpt2.b B = N
liminfequzmpt2.k φ K A
liminfequzmpt2.e φ K B
liminfequzmpt2.c φ j K C V
Assertion liminfequzmpt2 φ lim inf j A C = lim inf j B C

Proof

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