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 = ℤ_{\geq M}$
	climmpt.2	$⊢ G = (k \in Z ⟼ F (k))$
Assertion	climmpt	$⊢ (M \in ℤ \land F \in V) \to (F ⇝ A \leftrightarrow G ⇝ A)$

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

Metamath Proof Explorer