climeldmeqmpt

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

	Ref	Expression
Hypotheses	climeldmeqmpt.k	$⊢ Ⅎ k φ$
	climeldmeqmpt.m	$⊢ φ \to M \in ℤ$
	climeldmeqmpt.z	$⊢ Z = ℤ_{\geq M}$
	climeldmeqmpt.a	$⊢ φ \to A \in R$
	climeldmeqmpt.i	$⊢ φ \to Z \subseteq A$
	climeldmeqmpt.b	$⊢ (φ \land k \in A) \to B \in V$
	climeldmeqmpt.t	$⊢ φ \to C \in S$
	climeldmeqmpt.l	$⊢ φ \to Z \subseteq C$
	climeldmeqmpt.c	$⊢ (φ \land k \in C) \to D \in W$
	climeldmeqmpt.e	$⊢ (φ \land k \in Z) \to B = D$
Assertion	climeldmeqmpt	$⊢ φ \to ((k \in A ⟼ B) \in dom ⇝ \leftrightarrow (k \in C ⟼ D) \in dom ⇝)$

Proof

Step	Hyp	Ref	Expression
1		climeldmeqmpt.k	$⊢ Ⅎ k φ$
2		climeldmeqmpt.m	$⊢ φ \to M \in ℤ$
3		climeldmeqmpt.z	$⊢ Z = ℤ_{\geq M}$
4		climeldmeqmpt.a	$⊢ φ \to A \in R$
5		climeldmeqmpt.i	$⊢ φ \to Z \subseteq A$
6		climeldmeqmpt.b	$⊢ (φ \land k \in A) \to B \in V$
7		climeldmeqmpt.t	$⊢ φ \to C \in S$
8		climeldmeqmpt.l	$⊢ φ \to Z \subseteq C$
9		climeldmeqmpt.c	$⊢ (φ \land k \in C) \to D \in W$
10		climeldmeqmpt.e	$⊢ (φ \land k \in Z) \to B = D$
11	4	mptexd	$⊢ φ \to (k \in A ⟼ B) \in V$
12	7	mptexd	$⊢ φ \to (k \in C ⟼ D) \in V$
13		nfv	$⊢ Ⅎ k j \in Z$
14	1 13	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
15		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
16		nfcv	$⊢ \underline{Ⅎ} k j$
17	16	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ D$
18	15 17	nfeq	$⊢ Ⅎ k ⦋ j / k ⦌ B = ⦋ j / k ⦌ D$
19	14 18	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D)$
20		eleq1w	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
21	20	anbi2d	$⊢ k = j \to ((φ \land k \in Z) \leftrightarrow (φ \land j \in Z))$
22		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
23		csbeq1a	$⊢ k = j \to D = ⦋ j / k ⦌ D$
24	22 23	eqeq12d	$⊢ k = j \to (B = D \leftrightarrow ⦋ j / k ⦌ B = ⦋ j / k ⦌ D)$
25	21 24	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to B = D) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D))$
26	19 25 10	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D$
27	5	sselda	$⊢ (φ \land j \in Z) \to j \in A$
28		nfv	$⊢ Ⅎ k j \in A$
29	1 28	nfan	$⊢ Ⅎ k (φ \land j \in A)$
30		nfcv	$⊢ \underline{Ⅎ} k V$
31	15 30	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in V$
32	29 31	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ B \in V)$
33		eleq1w	$⊢ k = j \to (k \in A \leftrightarrow j \in A)$
34	33	anbi2d	$⊢ k = j \to ((φ \land k \in A) \leftrightarrow (φ \land j \in A))$
35	22	eleq1d	$⊢ k = j \to (B \in V \leftrightarrow ⦋ j / k ⦌ B \in V)$
36	34 35	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to B \in V) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ B \in V))$
37	32 36 6	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ B \in V$
38	27 37	syldan	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ B \in V$
39	16	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
40		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
41	16 39 22 40	fvmptf	$⊢ (j \in A \land ⦋ j / k ⦌ B \in V) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
42	27 38 41	syl2anc	$⊢ (φ \land j \in Z) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
43	8	sselda	$⊢ (φ \land j \in Z) \to j \in C$
44		nfv	$⊢ Ⅎ k j \in C$
45	1 44	nfan	$⊢ Ⅎ k (φ \land j \in C)$
46		nfcv	$⊢ \underline{Ⅎ} k W$
47	17 46	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ D \in W$
48	45 47	nfim	$⊢ Ⅎ k ((φ \land j \in C) \to ⦋ j / k ⦌ D \in W)$
49		eleq1w	$⊢ k = j \to (k \in C \leftrightarrow j \in C)$
50	49	anbi2d	$⊢ k = j \to ((φ \land k \in C) \leftrightarrow (φ \land j \in C))$
51	23	eleq1d	$⊢ k = j \to (D \in W \leftrightarrow ⦋ j / k ⦌ D \in W)$
52	50 51	imbi12d	$⊢ k = j \to (((φ \land k \in C) \to D \in W) \leftrightarrow ((φ \land j \in C) \to ⦋ j / k ⦌ D \in W))$
53	48 52 9	chvarfv	$⊢ (φ \land j \in C) \to ⦋ j / k ⦌ D \in W$
54	43 53	syldan	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ D \in W$
55		eqid	$⊢ (k \in C ⟼ D) = (k \in C ⟼ D)$
56	16 17 23 55	fvmptf	$⊢ (j \in C \land ⦋ j / k ⦌ D \in W) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
57	43 54 56	syl2anc	$⊢ (φ \land j \in Z) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
58	26 42 57	3eqtr4d	$⊢ (φ \land j \in Z) \to (k \in A ⟼ B) (j) = (k \in C ⟼ D) (j)$
59	3 11 12 2 58	climeldmeq	$⊢ φ \to ((k \in A ⟼ B) \in dom ⇝ \leftrightarrow (k \in C ⟼ D) \in dom ⇝)$

Metamath Proof Explorer

Theorem climeldmeqmpt

Proof