Metamath Proof Explorer

Theorem lo1bdd

Description: The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1bdd ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m

Proof

Step Hyp Ref Expression
1 simpl ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → F ∈ ≤𝑂⁡1
2 simpr ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → F : A ⟶ ℝ
3 fdm ⊢ F : A ⟶ ℝ → dom ⁡ F = A
4 3 adantl ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → dom ⁡ F = A
5 lo1dm ⊢ F ∈ ≤𝑂⁡1 → dom ⁡ F ⊆ ℝ
6 5 adantr ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → dom ⁡ F ⊆ ℝ
7 4 6 eqsstrrd ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → A ⊆ ℝ
8 ello12 ⊢ F : A ⟶ ℝ ∧ A ⊆ ℝ → F ∈ ≤𝑂⁡1 ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m
9 2 7 8 syl2anc ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → F ∈ ≤𝑂⁡1 ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m
10 1 9 mpbid ⊢ F ∈ ≤𝑂⁡1 ∧ F : A ⟶ ℝ → ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ A x ≤ y → F ⁡ y ≤ m