climeldmeqmpt3

Description: Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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

Metamath Proof Explorer

Theorem climeldmeqmpt3

Proof