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 ⊢Ⅎ_kk∈A⟼C
10 nfmpt1 ⊢Ⅎ_kk∈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