Metamath Proof Explorer

Theorem climfveq

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

Ref Expression
Hypotheses climfveq.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climfveq.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
climfveq.3 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
climfveq.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climfveq.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion climfveq ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 climfveq.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climfveq.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3 climfveq.3 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
4 climfveq.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 climfveq.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
6 climdm ⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
7 6 biimpi ⊢ ( 𝐹 ∈ dom ⇝ → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
9 8 6 sylibr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
10 1 2 3 4 5 climeldmeq ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
12 9 11 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
13 climdm ⊢ ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
14 12 13 sylib ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
15 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ 𝑊 )
16 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
18 5 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
20 1 15 16 17 19 climeq ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
21 14 20 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
22 climuni ⊢ ( ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
23 8 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
24 ndmfv ⊢ ( ¬ 𝐹 ∈ dom ⇝ → ( ⇝ ‘ 𝐹 ) = ∅ )
25 24 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ∅ )
26 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐹 ∈ dom ⇝ )
27 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
28 26 27 mtbid ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐺 ∈ dom ⇝ )
29 ndmfv ⊢ ( ¬ 𝐺 ∈ dom ⇝ → ( ⇝ ‘ 𝐺 ) = ∅ )
30 28 29 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) = ∅ )
31 25 30 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
32 23 31 pm2.61dan ⊢ ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )