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 \in 𝑂 (1) \to {F ↾}_{A} \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		resco	$⊢ {(abs \circ F) ↾}_{A} = abs \circ ({F ↾}_{A})$
2		o1f	$⊢ F \in 𝑂 (1) \to F : dom F ⟶ ℂ$
3		lo1o1	$⊢ F : dom F ⟶ ℂ \to (F \in 𝑂 (1) \leftrightarrow abs \circ F \in \leq 𝑂 (1))$
4	2 3	syl	$⊢ F \in 𝑂 (1) \to (F \in 𝑂 (1) \leftrightarrow abs \circ F \in \leq 𝑂 (1))$
5	4	ibi	$⊢ F \in 𝑂 (1) \to abs \circ F \in \leq 𝑂 (1)$
6		lo1res	$⊢ abs \circ F \in \leq 𝑂 (1) \to {(abs \circ F) ↾}_{A} \in \leq 𝑂 (1)$
7	5 6	syl	$⊢ F \in 𝑂 (1) \to {(abs \circ F) ↾}_{A} \in \leq 𝑂 (1)$
8	1 7	eqeltrrid	$⊢ F \in 𝑂 (1) \to abs \circ ({F ↾}_{A}) \in \leq 𝑂 (1)$
9		fresin	$⊢ F : dom F ⟶ ℂ \to ({F ↾}_{A}) : dom F \cap A ⟶ ℂ$
10		lo1o1	$⊢ ({F ↾}_{A}) : dom F \cap A ⟶ ℂ \to ({F ↾}_{A} \in 𝑂 (1) \leftrightarrow abs \circ ({F ↾}_{A}) \in \leq 𝑂 (1))$
11	2 9 10	3syl	$⊢ F \in 𝑂 (1) \to ({F ↾}_{A} \in 𝑂 (1) \leftrightarrow abs \circ ({F ↾}_{A}) \in \leq 𝑂 (1))$
12	8 11	mpbird	$⊢ F \in 𝑂 (1) \to {F ↾}_{A} \in 𝑂 (1)$