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

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 ( 𝐹 ∈ 𝑂(1) → ( 𝐹 ↾ 𝐴 ) ∈ 𝑂(1) )

Proof

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