This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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