Metamath Proof Explorer

Theorem o1res

Description: The restriction of an eventually bounded function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion o1res ⊢ F ∈ 𝑂⁡1 → F ↾ A ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 resco ⊢ abs ∘ F ↾ A = abs ∘ F ↾ A
2 o1f ⊢ F ∈ 𝑂⁡1 → F : dom ⁡ F ⟶ ℂ
3 lo1o1 ⊢ F : dom ⁡ F ⟶ ℂ → F ∈ 𝑂⁡1 ↔ abs ∘ F ∈ ≤𝑂⁡1
4 2 3 syl ⊢ F ∈ 𝑂⁡1 → F ∈ 𝑂⁡1 ↔ abs ∘ F ∈ ≤𝑂⁡1
5 4 ibi ⊢ F ∈ 𝑂⁡1 → abs ∘ F ∈ ≤𝑂⁡1
6 lo1res ⊢ abs ∘ F ∈ ≤𝑂⁡1 → abs ∘ F ↾ A ∈ ≤𝑂⁡1
7 5 6 syl ⊢ F ∈ 𝑂⁡1 → abs ∘ F ↾ A ∈ ≤𝑂⁡1
8 1 7 eqeltrrid ⊢ F ∈ 𝑂⁡1 → abs ∘ F ↾ A ∈ ≤𝑂⁡1
9 fresin ⊢ F : dom ⁡ F ⟶ ℂ → F ↾ A : dom ⁡ F ∩ A ⟶ ℂ
10 lo1o1 ⊢ F ↾ A : dom ⁡ F ∩ A ⟶ ℂ → F ↾ A ∈ 𝑂⁡1 ↔ abs ∘ F ↾ A ∈ ≤𝑂⁡1
11 2 9 10 3syl ⊢ F ∈ 𝑂⁡1 → F ↾ A ∈ 𝑂⁡1 ↔ abs ∘ F ↾ A ∈ ≤𝑂⁡1
12 8 11 mpbird ⊢ F ∈ 𝑂⁡1 → F ↾ A ∈ 𝑂⁡1