# Metamath Proof Explorer

## Theorem 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}\phantom{\rule{.4em}{0ex}}{\phi }$
climeldmeqmpt.m ${⊢}{\phi }\to {M}\in ℤ$
climeldmeqmpt.z ${⊢}{Z}={ℤ}_{\ge {M}}$
climeldmeqmpt.a ${⊢}{\phi }\to {A}\in {R}$
climeldmeqmpt.i ${⊢}{\phi }\to {Z}\subseteq {A}$
climeldmeqmpt.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {V}$
climeldmeqmpt.t ${⊢}{\phi }\to {C}\in {S}$
climeldmeqmpt.l ${⊢}{\phi }\to {Z}\subseteq {C}$
climeldmeqmpt.c ${⊢}\left({\phi }\wedge {k}\in {C}\right)\to {D}\in {W}$
climeldmeqmpt.e ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {B}={D}$
Assertion climeldmeqmpt ${⊢}{\phi }\to \left(\left({k}\in {A}⟼{B}\right)\in \mathrm{dom}⇝↔\left({k}\in {C}⟼{D}\right)\in \mathrm{dom}⇝\right)$

### Proof

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