Metamath Proof Explorer

Theorem lo1res2

Description: The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rlimres2.1 ⊢ φ → A ⊆ B
lo1res2.2 ⊢ φ → x ∈ B ⟼ C ∈ ≤𝑂⁡1
Assertion lo1res2 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 rlimres2.1 ⊢ φ → A ⊆ B
2 lo1res2.2 ⊢ φ → x ∈ B ⟼ C ∈ ≤𝑂⁡1
3 1 resmptd ⊢ φ → x ∈ B ⟼ C ↾ A = x ∈ A ⟼ C
4 lo1res ⊢ x ∈ B ⟼ C ∈ ≤𝑂⁡1 → x ∈ B ⟼ C ↾ A ∈ ≤𝑂⁡1
5 2 4 syl ⊢ φ → x ∈ B ⟼ C ↾ A ∈ ≤𝑂⁡1
6 3 5 eqeltrrd ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1