climeldmeqf

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climeldmeqf.p	$⊢ Ⅎ k φ$
	climeldmeqf.n	$⊢ \underline{Ⅎ} k F$
	climeldmeqf.o	$⊢ \underline{Ⅎ} k G$
	climeldmeqf.z	$⊢ Z = ℤ_{\geq M}$
	climeldmeqf.f	$⊢ φ \to F \in V$
	climeldmeqf.g	$⊢ φ \to G \in W$
	climeldmeqf.m	$⊢ φ \to M \in ℤ$
	climeldmeqf.e	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
Assertion	climeldmeqf	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$

Proof

Step	Hyp	Ref	Expression
1		climeldmeqf.p	$⊢ Ⅎ k φ$
2		climeldmeqf.n	$⊢ \underline{Ⅎ} k F$
3		climeldmeqf.o	$⊢ \underline{Ⅎ} k G$
4		climeldmeqf.z	$⊢ Z = ℤ_{\geq M}$
5		climeldmeqf.f	$⊢ φ \to F \in V$
6		climeldmeqf.g	$⊢ φ \to G \in W$
7		climeldmeqf.m	$⊢ φ \to M \in ℤ$
8		climeldmeqf.e	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
9		nfv	$⊢ Ⅎ k j \in Z$
10	1 9	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
11		nfcv	$⊢ \underline{Ⅎ} k j$
12	2 11	nffv	$⊢ \underline{Ⅎ} k F (j)$
13	3 11	nffv	$⊢ \underline{Ⅎ} k G (j)$
14	12 13	nfeq	$⊢ Ⅎ k F (j) = G (j)$
15	10 14	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to F (j) = G (j))$
16		eleq1w	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
17	16	anbi2d	$⊢ k = j \to ((φ \land k \in Z) \leftrightarrow (φ \land j \in Z))$
18		fveq2	$⊢ k = j \to F (k) = F (j)$
19		fveq2	$⊢ k = j \to G (k) = G (j)$
20	18 19	eqeq12d	$⊢ k = j \to (F (k) = G (k) \leftrightarrow F (j) = G (j))$
21	17 20	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to F (k) = G (k)) \leftrightarrow ((φ \land j \in Z) \to F (j) = G (j)))$
22	15 21 8	chvarfv	$⊢ (φ \land j \in Z) \to F (j) = G (j)$
23	4 5 6 7 22	climeldmeq	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$

Metamath Proof Explorer

Theorem climeldmeqf

Proof