Theorem climmpt

Description: Exhibit a function G with the same convergence properties as the not-quite-function F . (Contributed by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	2clim.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climmpt.2	$$⊢G=\left(k\in Z⟼F\left(k\right)\right)$$
Assertion	climmpt	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(F⇝A\leftrightarrow G⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		2clim.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climmpt.2	$$⊢G=\left(k\in Z⟼F\left(k\right)\right)$$
3		simpr	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to F\in V$$
4		fvex	$$⊢{\mathbb{Z}}_{\ge M}\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢Z\in \mathrm{V}$$
6	5	mptex	$$⊢\left(k\in Z⟼F\left(k\right)\right)\in \mathrm{V}$$
7	2 6	eqeltri	$$⊢G\in \mathrm{V}$$
8	7	a1i	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to G\in \mathrm{V}$$
9		simpl	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to M\in \mathbb{Z}$$
10		fveq2	$$⊢k=m\to F\left(k\right)=F\left(m\right)$$
11		fvex	$$⊢F\left(m\right)\in \mathrm{V}$$
12	10 2 11	fvmpt	$$⊢m\in Z\to G\left(m\right)=F\left(m\right)$$
13	12	eqcomd	$$⊢m\in Z\to F\left(m\right)=G\left(m\right)$$
14	13	adantl	$$⊢\left(\left(M\in \mathbb{Z}\wedge F\in V\right)\wedge m\in Z\right)\to F\left(m\right)=G\left(m\right)$$
15	1 3 8 9 14	climeq	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(F⇝A\leftrightarrow G⇝A\right)$$