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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climmpt.2	⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
Assertion	climmpt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		2clim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climmpt.2	⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
3		simpr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ 𝑉 )
4		fvex	⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
5	1 4	eqeltri	⊢ 𝑍 ∈ V
6	5	mptex	⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ∈ V
7	2 6	eqeltri	⊢ 𝐺 ∈ V
8	7	a1i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐺 ∈ V )
9		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝑀 ∈ ℤ )
10		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
11		fvex	⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
12	10 2 11	fvmpt	⊢ ( 𝑚 ∈ 𝑍 → ( 𝐺 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
13	12	eqcomd	⊢ ( 𝑚 ∈ 𝑍 → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
14	13	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
15	1 3 8 9 14	climeq	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )