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 ⊢ Ⅎ 𝑥 𝜑
climeqmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
climeqmpt.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
climeqmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climeqmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climeqmpt.s ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
climeqmpt.t ⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
climeqmpt.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
Assertion climeqmpt ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝ 𝐷 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 climeqmpt.x ⊢ Ⅎ 𝑥 𝜑
2 climeqmpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 climeqmpt.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 climeqmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 climeqmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6 climeqmpt.s ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7 climeqmpt.t ⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
8 climeqmpt.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
9 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
10 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
11 2 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ V )
12 3 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑍 ⊆ 𝐴 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝑍 )
15 13 14 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝐴 )
16 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
17 16 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
18 15 8 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
19 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑍 ⊆ 𝐵 )
20 19 14 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝐵 )
21 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
22 21 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
23 20 8 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
24 23 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐶 = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) )
25 18 24 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) )
26 1 9 10 4 5 11 12 25 climeqf ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝ 𝐷 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝ 𝐷 ) )