Theorem lo1bdd

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

	Ref	Expression
Assertion	lo1bdd	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → 𝐹 ∈ ≤𝑂(1) )
2		simpr	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ )
3		fdm	⊢ ( 𝐹 : 𝐴 ⟶ ℝ → dom 𝐹 = 𝐴 )
4	3	adantl	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → dom 𝐹 = 𝐴 )
5		lo1dm	⊢ ( 𝐹 ∈ ≤𝑂(1) → dom 𝐹 ⊆ ℝ )
6	5	adantr	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → dom 𝐹 ⊆ ℝ )
7	4 6	eqsstrrd	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → 𝐴 ⊆ ℝ )
8		ello12	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
9	2 7 8	syl2anc	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
10	1 9	mpbid	⊢ ( ( 𝐹 ∈ ≤𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )