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	$$⊢\underset{\_}{Ⅎ}kF$$
	climmptf.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climmptf.f	$$⊢\phi \to F\in V$$
	climmptf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climmptf.g	$$⊢G=\left(k\in Z⟼F\left(k\right)\right)$$
Assertion	climmptf	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climmptf.k	$$⊢\underset{\_}{Ⅎ}kF$$
2		climmptf.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		climmptf.f	$$⊢\phi \to F\in V$$
4		climmptf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		climmptf.g	$$⊢G=\left(k\in Z⟼F\left(k\right)\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}jF\left(k\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
8	1 7	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
9		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
10	6 8 9	cbvmpt	$$⊢\left(k\in Z⟼F\left(k\right)\right)=\left(j\in Z⟼F\left(j\right)\right)$$
11	5 10	eqtri	$$⊢G=\left(j\in Z⟼F\left(j\right)\right)$$
12	4 11	climmpt	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(F⇝A\leftrightarrow G⇝A\right)$$
13	2 3 12	syl2anc	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$