This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climeldmeqmpt2

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climeldmeqmpt2.k ⊢ Ⅎ 𝑘 𝜑
climeldmeqmpt2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climeldmeqmpt2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climeldmeqmpt2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
climeldmeqmpt2.t ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
climeldmeqmpt2.i ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
climeldmeqmpt2.l ⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
climeldmeqmpt2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
Assertion climeldmeqmpt2 ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∈ dom ⇝ ↔ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ∈ dom ⇝ ) )

Proof

Step Hyp Ref Expression
1 climeldmeqmpt2.k ⊢ Ⅎ 𝑘 𝜑
2 climeldmeqmpt2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climeldmeqmpt2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 climeldmeqmpt2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
5 climeldmeqmpt2.t ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
6 climeldmeqmpt2.i ⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7 climeldmeqmpt2.l ⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
8 climeldmeqmpt2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
9 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
10 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
11 4 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∈ V )
12 5 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
13 6 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝐴 )
14 fvmpt4 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
15 13 8 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
16 7 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝐵 )
17 fvmpt4 ⊢ ( ( 𝑘 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
18 16 8 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
19 15 18 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) )
20 1 9 10 3 11 12 2 19 climeldmeqf ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∈ dom ⇝ ↔ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ∈ dom ⇝ ) )