Metamath Proof Explorer

Theorem climfveqmpt2

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

Ref Expression
Hypotheses climfveqmpt2.k ⊢ Ⅎ k φ
climfveqmpt2.m ⊢ φ → M ∈ ℤ
climfveqmpt2.z ⊢ Z = ℤ ≥ M
climfveqmpt2.a ⊢ φ → A ∈ V
climfveqmpt2.c ⊢ φ → B ∈ W
climfveqmpt2.s ⊢ φ → Z ⊆ A
climfveqmpt2.i ⊢ φ → Z ⊆ B
climfveqmpt2.b ⊢ φ ∧ k ∈ Z → C ∈ U
Assertion climfveqmpt2 ⊢ φ → ⇝ ⁡ k ∈ A ⟼ C = ⇝ ⁡ k ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 climfveqmpt2.k ⊢ Ⅎ k φ
2 climfveqmpt2.m ⊢ φ → M ∈ ℤ
3 climfveqmpt2.z ⊢ Z = ℤ ≥ M
4 climfveqmpt2.a ⊢ φ → A ∈ V
5 climfveqmpt2.c ⊢ φ → B ∈ W
6 climfveqmpt2.s ⊢ φ → Z ⊆ A
7 climfveqmpt2.i ⊢ φ → Z ⊆ B
8 climfveqmpt2.b ⊢ φ ∧ k ∈ Z → C ∈ U
9 nfmpt1 ⊢ Ⅎ _ k k ∈ A ⟼ C
10 nfmpt1 ⊢ Ⅎ _ k k ∈ B ⟼ C
11 4 mptexd ⊢ φ → k ∈ A ⟼ C ∈ V
12 5 mptexd ⊢ φ → k ∈ B ⟼ C ∈ V
13 6 sselda ⊢ φ ∧ k ∈ Z → k ∈ A
14 eqid ⊢ k ∈ A ⟼ C = k ∈ A ⟼ C
15 14 fvmpt2 ⊢ k ∈ A ∧ C ∈ U → k ∈ A ⟼ C ⁡ k = C
16 13 8 15 syl2anc ⊢ φ ∧ k ∈ Z → k ∈ A ⟼ C ⁡ k = C
17 7 sselda ⊢ φ ∧ k ∈ Z → k ∈ B
18 eqid ⊢ k ∈ B ⟼ C = k ∈ B ⟼ C
19 18 fvmpt2 ⊢ k ∈ B ∧ C ∈ U → k ∈ B ⟼ C ⁡ k = C
20 17 8 19 syl2anc ⊢ φ ∧ k ∈ Z → k ∈ B ⟼ C ⁡ k = C
21 16 20 eqtr4d ⊢ φ ∧ k ∈ Z → k ∈ A ⟼ C ⁡ k = k ∈ B ⟼ C ⁡ k
22 1 9 10 3 11 12 2 21 climfveqf ⊢ φ → ⇝ ⁡ k ∈ A ⟼ C = ⇝ ⁡ k ∈ B ⟼ C