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 ⊢ Ⅎ k φ
climeldmeqmpt2.m ⊢ φ → M ∈ ℤ
climeldmeqmpt2.z ⊢ Z = ℤ ≥ M
climeldmeqmpt2.a ⊢ φ → A ∈ W
climeldmeqmpt2.t ⊢ φ → B ∈ V
climeldmeqmpt2.i ⊢ φ → Z ⊆ A
climeldmeqmpt2.l ⊢ φ → Z ⊆ B
climeldmeqmpt2.b ⊢ φ ∧ k ∈ Z → C ∈ U
Assertion climeldmeqmpt2 ⊢ φ → k ∈ A ⟼ C ∈ dom ⁡ ⇝ ↔ k ∈ B ⟼ C ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 climeldmeqmpt2.k ⊢ Ⅎ k φ
2 climeldmeqmpt2.m ⊢ φ → M ∈ ℤ
3 climeldmeqmpt2.z ⊢ Z = ℤ ≥ M
4 climeldmeqmpt2.a ⊢ φ → A ∈ W
5 climeldmeqmpt2.t ⊢ φ → B ∈ V
6 climeldmeqmpt2.i ⊢ φ → Z ⊆ A
7 climeldmeqmpt2.l ⊢ φ → Z ⊆ B
8 climeldmeqmpt2.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 fvmpt4 ⊢ k ∈ A ∧ C ∈ U → k ∈ A ⟼ C ⁡ k = C
15 13 8 14 syl2anc ⊢ φ ∧ k ∈ Z → k ∈ A ⟼ C ⁡ k = C
16 7 sselda ⊢ φ ∧ k ∈ Z → k ∈ B
17 fvmpt4 ⊢ k ∈ B ∧ C ∈ U → k ∈ B ⟼ C ⁡ k = C
18 16 8 17 syl2anc ⊢ φ ∧ k ∈ Z → k ∈ B ⟼ C ⁡ k = C
19 15 18 eqtr4d ⊢ φ ∧ k ∈ Z → k ∈ A ⟼ C ⁡ k = k ∈ B ⟼ C ⁡ k
20 1 9 10 3 11 12 2 19 climeldmeqf ⊢ φ → k ∈ A ⟼ C ∈ dom ⁡ ⇝ ↔ k ∈ B ⟼ C ∈ dom ⁡ ⇝