Metamath Proof Explorer


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 eqtr3id ( 𝐹 ∈ ≤𝑂(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) )