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
|- F/ n ph
smflimsuplem5.b
|- F/ m ph
smflimsuplem5.m
|- ( ph -> M e. ZZ )
smflimsuplem5.z
|- Z = ( ZZ>= ` M )
smflimsuplem5.s
|- ( ph -> S e. SAlg )
smflimsuplem5.f
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsuplem5.e
|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
smflimsuplem5.h
|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
smflimsuplem5.r
|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
smflimsuplem5.n
|- ( ph -> N e. Z )
smflimsuplem5.x
|- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) )
Assertion smflimsuplem5
|- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) )

Proof

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