Metamath Proof Explorer

Theorem climeqmpt

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climeqmpt.x ⊢ Ⅎ x φ
climeqmpt.a ⊢ φ → A ∈ V
climeqmpt.b ⊢ φ → B ∈ W
climeqmpt.m ⊢ φ → M ∈ ℤ
climeqmpt.z ⊢ Z = ℤ ≥ M
climeqmpt.s ⊢ φ → Z ⊆ A
climeqmpt.t ⊢ φ → Z ⊆ B
climeqmpt.c ⊢ φ ∧ x ∈ Z → C ∈ U
Assertion climeqmpt ⊢ φ → x ∈ A ⟼ C ⇝ D ↔ x ∈ B ⟼ C ⇝ D

Proof

Step Hyp Ref Expression
1 climeqmpt.x ⊢ Ⅎ x φ
2 climeqmpt.a ⊢ φ → A ∈ V
3 climeqmpt.b ⊢ φ → B ∈ W
4 climeqmpt.m ⊢ φ → M ∈ ℤ
5 climeqmpt.z ⊢ Z = ℤ ≥ M
6 climeqmpt.s ⊢ φ → Z ⊆ A
7 climeqmpt.t ⊢ φ → Z ⊆ B
8 climeqmpt.c ⊢ φ ∧ x ∈ Z → C ∈ U
9 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ C
10 nfmpt1 ⊢ Ⅎ _ x x ∈ B ⟼ C
11 2 mptexd ⊢ φ → x ∈ A ⟼ C ∈ V
12 3 mptexd ⊢ φ → x ∈ B ⟼ C ∈ V
13 6 adantr ⊢ φ ∧ x ∈ Z → Z ⊆ A
14 simpr ⊢ φ ∧ x ∈ Z → x ∈ Z
15 13 14 sseldd ⊢ φ ∧ x ∈ Z → x ∈ A
16 eqid ⊢ x ∈ A ⟼ C = x ∈ A ⟼ C
17 16 fvmpt2 ⊢ x ∈ A ∧ C ∈ U → x ∈ A ⟼ C ⁡ x = C
18 15 8 17 syl2anc ⊢ φ ∧ x ∈ Z → x ∈ A ⟼ C ⁡ x = C
19 7 adantr ⊢ φ ∧ x ∈ Z → Z ⊆ B
20 19 14 sseldd ⊢ φ ∧ x ∈ Z → x ∈ B
21 eqid ⊢ x ∈ B ⟼ C = x ∈ B ⟼ C
22 21 fvmpt2 ⊢ x ∈ B ∧ C ∈ U → x ∈ B ⟼ C ⁡ x = C
23 20 8 22 syl2anc ⊢ φ ∧ x ∈ Z → x ∈ B ⟼ C ⁡ x = C
24 23 eqcomd ⊢ φ ∧ x ∈ Z → C = x ∈ B ⟼ C ⁡ x
25 18 24 eqtrd ⊢ φ ∧ x ∈ Z → x ∈ A ⟼ C ⁡ x = x ∈ B ⟼ C ⁡ x
26 1 9 10 4 5 11 12 25 climeqf ⊢ φ → x ∈ A ⟼ C ⇝ D ↔ x ∈ B ⟼ C ⇝ D