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	⊢ Ⅎ 𝑘 𝐹
	climmptf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climmptf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climmptf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climmptf.g	⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
Assertion	climmptf	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climmptf.k	⊢ Ⅎ 𝑘 𝐹
2		climmptf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climmptf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4		climmptf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		climmptf.g	⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
6		nfcv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑘 )
7		nfcv	⊢ Ⅎ 𝑘 𝑗
8	1 7	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
9		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
10	6 8 9	cbvmpt	⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) )
11	5 10	eqtri	⊢ 𝐺 = ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) )
12	4 11	climmpt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )
13	2 3 12	syl2anc	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )