Metamath Proof Explorer


Theorem smflimsuplem5

Description: H converges to the superior limit of F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem5.a n φ
smflimsuplem5.b m φ
smflimsuplem5.m φ M
smflimsuplem5.z Z = M
smflimsuplem5.s φ S SAlg
smflimsuplem5.f φ F : Z SMblFn S
smflimsuplem5.e E = n Z x m n dom F m | sup ran m n F m x * <
smflimsuplem5.h H = n Z x E n sup ran m n F m x * <
smflimsuplem5.r φ lim sup m Z F m X
smflimsuplem5.n φ N Z
smflimsuplem5.x φ X m N dom F m
Assertion smflimsuplem5 φ n N H n X lim sup m N F m X

Proof

Step Hyp Ref Expression
1 smflimsuplem5.a n φ
2 smflimsuplem5.b m φ
3 smflimsuplem5.m φ M
4 smflimsuplem5.z Z = M
5 smflimsuplem5.s φ S SAlg
6 smflimsuplem5.f φ F : Z SMblFn S
7 smflimsuplem5.e E = n Z x m n dom F m | sup ran m n F m x * <
8 smflimsuplem5.h H = n Z x E n sup ran m n F m x * <
9 smflimsuplem5.r φ lim sup m Z F m X
10 smflimsuplem5.n φ N Z
11 smflimsuplem5.x φ X m N dom F m
12 4 eleq2i N Z N M
13 12 biimpi N Z N M
14 uzss N M N M
15 13 14 syl N Z N M
16 15 4 sseqtrrdi N Z N Z
17 10 16 syl φ N Z
18 17 sselda φ n N n Z
19 nfcv _ x Z
20 nfrab1 _ x x m n dom F m | sup ran m n F m x * <
21 19 20 nfmpt _ x n Z x m n dom F m | sup ran m n F m x * <
22 7 21 nfcxfr _ x E
23 nfcv _ x n
24 22 23 nffv _ x E n
25 fvex E n V
26 24 25 mptexf x E n sup ran m n F m x * < V
27 26 a1i φ n N x E n sup ran m n F m x * < V
28 8 fvmpt2 n Z x E n sup ran m n F m x * < V H n = x E n sup ran m n F m x * <
29 18 27 28 syl2anc φ n N H n = x E n sup ran m n F m x * <
30 29 fveq1d φ n N H n X = x E n sup ran m n F m x * < X
31 nfcv _ y E n
32 nfcv _ y sup ran m n F m x * <
33 nfcv _ x sup ran m n F m y * <
34 fveq2 x = y F m x = F m y
35 34 mpteq2dv x = y m n F m x = m n F m y
36 35 rneqd x = y ran m n F m x = ran m n F m y
37 36 supeq1d x = y sup ran m n F m x * < = sup ran m n F m y * <
38 24 31 32 33 37 cbvmptf x E n sup ran m n F m x * < = y E n sup ran m n F m y * <
39 simpl y = X m n y = X
40 39 fveq2d y = X m n F m y = F m X
41 40 mpteq2dva y = X m n F m y = m n F m X
42 41 rneqd y = X ran m n F m y = ran m n F m X
43 42 supeq1d y = X sup ran m n F m y * < = sup ran m n F m X * <
44 43 eleq1d y = X sup ran m n F m y * < sup ran m n F m X * <
45 uzss n N n N
46 iinss1 n N m N dom F m m n dom F m
47 45 46 syl n N m N dom F m m n dom F m
48 47 adantl φ n N m N dom F m m n dom F m
49 11 adantr φ n N X m N dom F m
50 48 49 sseldd φ n N X m n dom F m
51 nfv m n N
52 2 51 nfan m φ n N
53 eqid n = n
54 simpll φ n N m n φ
55 45 sselda n N m n m N
56 55 adantll φ n N m n m N
57 5 adantr φ m N S SAlg
58 simpl φ m N φ
59 17 sselda φ m N m Z
60 6 ffvelrnda φ m Z F m SMblFn S
61 58 59 60 syl2anc φ m N F m SMblFn S
62 eqid dom F m = dom F m
63 57 61 62 smff φ m N F m : dom F m
64 eliin X m N dom F m X m N dom F m m N X dom F m
65 11 64 syl φ X m N dom F m m N X dom F m
66 11 65 mpbid φ m N X dom F m
67 66 adantr φ m N m N X dom F m
68 simpr φ m N m N
69 rspa m N X dom F m m N X dom F m
70 67 68 69 syl2anc φ m N X dom F m
71 63 70 ffvelrnd φ m N F m X
72 54 56 71 syl2anc φ n N m n F m X
73 eluzelz n N n
74 73 adantl φ n N n
75 3 adantr φ n N M
76 fvex F m X V
77 76 a1i φ n N m Z F m X V
78 52 74 75 53 4 72 77 limsupequzmpt φ n N lim sup m n F m X = lim sup m Z F m X
79 9 adantr φ n N lim sup m Z F m X
80 78 79 eqeltrd φ n N lim sup m n F m X
81 80 renepnfd φ n N lim sup m n F m X +∞
82 52 53 72 81 limsupubuzmpt φ n N y m n F m X y
83 uzid2 n N n n
84 83 ne0d n N n
85 84 adantl φ n N n
86 52 85 72 supxrre3rnmpt φ n N sup ran m n F m X * < y m n F m X y
87 82 86 mpbird φ n N sup ran m n F m X * <
88 44 50 87 elrabd φ n N X y m n dom F m | sup ran m n F m y * <
89 simpl y = x m n y = x
90 89 fveq2d y = x m n F m y = F m x
91 90 mpteq2dva y = x m n F m y = m n F m x
92 91 rneqd y = x ran m n F m y = ran m n F m x
93 92 supeq1d y = x sup ran m n F m y * < = sup ran m n F m x * <
94 93 eleq1d y = x sup ran m n F m y * < sup ran m n F m x * <
95 94 cbvrabv y m n dom F m | sup ran m n F m y * < = x m n dom F m | sup ran m n F m x * <
96 88 95 eleqtrdi φ n N X x m n dom F m | sup ran m n F m x * <
97 eqid x m n dom F m | sup ran m n F m x * < = x m n dom F m | sup ran m n F m x * <
98 fvex F m V
99 98 dmex dom F m V
100 99 rgenw m n dom F m V
101 100 a1i n N m n dom F m V
102 84 101 iinexd n N m n dom F m V
103 102 adantl φ n N m n dom F m V
104 97 103 rabexd φ n N x m n dom F m | sup ran m n F m x * < V
105 7 fvmpt2 n Z x m n dom F m | sup ran m n F m x * < V E n = x m n dom F m | sup ran m n F m x * <
106 18 104 105 syl2anc φ n N E n = x m n dom F m | sup ran m n F m x * <
107 96 106 eleqtrrd φ n N X E n
108 38 43 107 87 fvmptd3 φ n N x E n sup ran m n F m x * < X = sup ran m n F m X * <
109 30 108 eqtrd φ n N H n X = sup ran m n F m X * <
110 1 109 mpteq2da φ n N H n X = n N sup ran m n F m X * <
111 4 eluzelz2 N Z N
112 10 111 syl φ N
113 eqid N = N
114 76 a1i φ m N F m X V
115 76 a1i φ m Z F m X V
116 2 112 3 113 4 114 115 limsupequzmpt φ lim sup m N F m X = lim sup m Z F m X
117 116 9 eqeltrd φ lim sup m N F m X
118 2 112 113 71 117 supcnvlimsupmpt φ n N sup ran m n F m X * < lim sup m N F m X
119 110 118 eqbrtrd φ n N H n X lim sup m N F m X