lo1res

Description: The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	lo1res	$⊢ F \in \leq 𝑂 (1) \to {F ↾}_{A} \in \leq 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		lo1f	$⊢ F \in \leq 𝑂 (1) \to F : dom F ⟶ ℝ$
2		lo1bdd	$⊢ (F \in \leq 𝑂 (1) \land F : dom F ⟶ ℝ) \to \exists x \in ℝ \exists m \in ℝ \forall y \in dom F (x \leq y \to F (y) \leq m)$
3	1 2	mpdan	$⊢ F \in \leq 𝑂 (1) \to \exists x \in ℝ \exists m \in ℝ \forall y \in dom F (x \leq y \to F (y) \leq m)$
4		inss1	$⊢ dom F \cap A \subseteq dom F$
5		ssralv	$⊢ dom F \cap A \subseteq dom F \to (\forall y \in dom F (x \leq y \to F (y) \leq m) \to \forall y \in (dom F \cap A) (x \leq y \to F (y) \leq m))$
6	4 5	ax-mp	$⊢ \forall y \in dom F (x \leq y \to F (y) \leq m) \to \forall y \in (dom F \cap A) (x \leq y \to F (y) \leq m)$
7		elinel2	$⊢ y \in (dom F \cap A) \to y \in A$
8	7	fvresd	$⊢ y \in (dom F \cap A) \to ({F ↾}_{A}) (y) = F (y)$
9	8	breq1d	$⊢ y \in (dom F \cap A) \to (({F ↾}_{A}) (y) \leq m \leftrightarrow F (y) \leq m)$
10	9	imbi2d	$⊢ y \in (dom F \cap A) \to ((x \leq y \to ({F ↾}_{A}) (y) \leq m) \leftrightarrow (x \leq y \to F (y) \leq m))$
11	10	ralbiia	$⊢ \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m) \leftrightarrow \forall y \in (dom F \cap A) (x \leq y \to F (y) \leq m)$
12	6 11	sylibr	$⊢ \forall y \in dom F (x \leq y \to F (y) \leq m) \to \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m)$
13	12	reximi	$⊢ \exists m \in ℝ \forall y \in dom F (x \leq y \to F (y) \leq m) \to \exists m \in ℝ \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m)$
14	13	reximi	$⊢ \exists x \in ℝ \exists m \in ℝ \forall y \in dom F (x \leq y \to F (y) \leq m) \to \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m)$
15	3 14	syl	$⊢ F \in \leq 𝑂 (1) \to \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m)$
16		fssres	$⊢ (F : dom F ⟶ ℝ \land dom F \cap A \subseteq dom F) \to ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ ℝ$
17	1 4 16	sylancl	$⊢ F \in \leq 𝑂 (1) \to ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ ℝ$
18		resres	$⊢ {({F ↾}_{dom F}) ↾}_{A} = {F ↾}_{(dom F \cap A)}$
19		ffn	$⊢ F : dom F ⟶ ℝ \to F Fn dom F$
20		fnresdm	$⊢ F Fn dom F \to {F ↾}_{dom F} = F$
21	1 19 20	3syl	$⊢ F \in \leq 𝑂 (1) \to {F ↾}_{dom F} = F$
22	21	reseq1d	$⊢ F \in \leq 𝑂 (1) \to {({F ↾}_{dom F}) ↾}_{A} = {F ↾}_{A}$
23	18 22	eqtr3id	$⊢ F \in \leq 𝑂 (1) \to {F ↾}_{(dom F \cap A)} = {F ↾}_{A}$
24	23	feq1d	$⊢ F \in \leq 𝑂 (1) \to (({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ ℝ \leftrightarrow ({F ↾}_{A}) : dom F \cap A ⟶ ℝ)$
25	17 24	mpbid	$⊢ F \in \leq 𝑂 (1) \to ({F ↾}_{A}) : dom F \cap A ⟶ ℝ$
26		lo1dm	$⊢ F \in \leq 𝑂 (1) \to dom F \subseteq ℝ$
27	4 26	sstrid	$⊢ F \in \leq 𝑂 (1) \to dom F \cap A \subseteq ℝ$
28		ello12	$⊢ (({F ↾}_{A}) : dom F \cap A ⟶ ℝ \land dom F \cap A \subseteq ℝ) \to ({F ↾}_{A} \in \leq 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m))$
29	25 27 28	syl2anc	$⊢ F \in \leq 𝑂 (1) \to ({F ↾}_{A} \in \leq 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap A) (x \leq y \to ({F ↾}_{A}) (y) \leq m))$
30	15 29	mpbird	$⊢ F \in \leq 𝑂 (1) \to {F ↾}_{A} \in \leq 𝑂 (1)$

Metamath Proof Explorer

Theorem lo1res

Proof