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) )