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

Proof

Step	Hyp	Ref	Expression
1		lo1f	⊢ ( 𝐹 ∈ ≤𝑂(1) → 𝐹 : dom 𝐹 ⟶ ℝ )
2		lo1bdd	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : dom 𝐹 ⟶ ℝ ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
3	1 2	mpdan	⊢ ( 𝐹 ∈ ≤𝑂(1) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
4		inss1	⊢ ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹
5		ssralv	⊢ ( ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹 → ( ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) → ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
6	4 5	ax-mp	⊢ ( ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) → ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
7		elinel2	⊢ ( 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) → 𝑦 ∈ 𝐴 )
8	7	fvresd	⊢ ( 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
9	8	breq1d	⊢ ( 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
10	9	imbi2d	⊢ ( 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) → ( ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) ↔ ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
11	10	ralbiia	⊢ ( ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) ↔ ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
12	6 11	sylibr	⊢ ( ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) → ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) )
13	12	reximi	⊢ ( ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) )
14	13	reximi	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) )
15	3 14	syl	⊢ ( 𝐹 ∈ ≤𝑂(1) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) )
16		fssres	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ )
17	1 4 16	sylancl	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ )
18		resres	⊢ ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐴 ) = ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) )
19		ffn	⊢ ( 𝐹 : dom 𝐹 ⟶ ℝ → 𝐹 Fn dom 𝐹 )
20		fnresdm	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
21	1 19 20	3syl	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
22	21	reseq1d	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐴 ) = ( 𝐹 ↾ 𝐴 ) )
23	18 22	syl5eqr	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) = ( 𝐹 ↾ 𝐴 ) )
24	23	feq1d	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ ↔ ( 𝐹 ↾ 𝐴 ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ ) )
25	17 24	mpbid	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ 𝐴 ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ )
26		lo1dm	⊢ ( 𝐹 ∈ ≤𝑂(1) → dom 𝐹 ⊆ ℝ )
27	4 26	sstrid	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( dom 𝐹 ∩ 𝐴 ) ⊆ ℝ )
28		ello12	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ ∧ ( dom 𝐹 ∩ 𝐴 ) ⊆ ℝ ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
29	25 27 28	syl2anc	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( ( 𝐹 ↾ 𝐴 ) ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ 𝐴 ) ( 𝑥 ≤ 𝑦 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ 𝑚 ) ) )
30	15 29	mpbird	⊢ ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ 𝐴 ) ∈ ≤𝑂(1) )