Metamath Proof Explorer

Theorem rlimi2

Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rlimi.1 ⊢ φ → ∀ z ∈ A B ∈ V
rlimi.2 ⊢ φ → R ∈ ℝ +
rlimi.3 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C
rlimi.4 ⊢ φ → D ∈ ℝ
Assertion rlimi2 ⊢ φ → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < R

Proof

Step Hyp Ref Expression
1 rlimi.1 ⊢ φ → ∀ z ∈ A B ∈ V
2 rlimi.2 ⊢ φ → R ∈ ℝ +
3 rlimi.3 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C
4 rlimi.4 ⊢ φ → D ∈ ℝ
5 1 2 3 rlimi ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < R
6 eqid ⊢ z ∈ A ⟼ B = z ∈ A ⟼ B
7 6 fnmpt ⊢ ∀ z ∈ A B ∈ V → z ∈ A ⟼ B Fn A
8 fndm ⊢ z ∈ A ⟼ B Fn A → dom ⁡ z ∈ A ⟼ B = A
9 1 7 8 3syl ⊢ φ → dom ⁡ z ∈ A ⟼ B = A
10 rlimss ⊢ z ∈ A ⟼ B ⇝ℝ C → dom ⁡ z ∈ A ⟼ B ⊆ ℝ
11 3 10 syl ⊢ φ → dom ⁡ z ∈ A ⟼ B ⊆ ℝ
12 9 11 eqsstrrd ⊢ φ → A ⊆ ℝ
13 rexico ⊢ A ⊆ ℝ ∧ D ∈ ℝ → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < R ↔ ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < R
14 12 4 13 syl2anc ⊢ φ → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < R ↔ ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < R
15 5 14 mpbird ⊢ φ → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < R