Theorem climmptf

Description: Exhibit a function G with the same convergence properties as the not-quite-function F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climmptf.k	|- F/_ k F
	climmptf.m	|- ( ph -> M e. ZZ )
	climmptf.f	|- ( ph -> F e. V )
	climmptf.z	|- Z = ( ZZ>= ` M )
	climmptf.g	|- G = ( k e. Z |-> ( F ` k ) )
Assertion	climmptf	|- ( ph -> ( F ~~> A <-> G ~~> A ) )

Proof

Step	Hyp	Ref	Expression
1		climmptf.k	|- F/_ k F
2		climmptf.m	|- ( ph -> M e. ZZ )
3		climmptf.f	|- ( ph -> F e. V )
4		climmptf.z	|- Z = ( ZZ>= ` M )
5		climmptf.g	|- G = ( k e. Z |-> ( F ` k ) )
6		nfcv	|- F/_ j ( F ` k )
7		nfcv	|- F/_ k j
8	1 7	nffv	|- F/_ k ( F ` j )
9		fveq2	|- ( k = j -> ( F ` k ) = ( F ` j ) )
10	6 8 9	cbvmpt	|- ( k e. Z |-> ( F ` k ) ) = ( j e. Z |-> ( F ` j ) )
11	5 10	eqtri	|- G = ( j e. Z |-> ( F ` j ) )
12	4 11	climmpt	|- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )
13	2 3 12	syl2anc	|- ( ph -> ( F ~~> A <-> G ~~> A ) )