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

Metamath Proof Explorer

Theorem ello12r

Description: Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion ello12r ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) → 𝐹 ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 ≤ 𝑥 ↔ 𝐶 ≤ 𝑥 ) )
2 1 imbi1d ⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ) )
3 2 ralbidv ⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ) )
4 breq2 ⊢ ( 𝑚 = 𝑀 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) )
5 4 imbi2d ⊢ ( 𝑚 = 𝑀 → ( ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) )
6 5 ralbidv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) )
7 3 6 rspc2ev ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
8 7 3expa ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
9 8 3adant1 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) )
10 ello12 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ) )
11 10 3ad2ant1 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑚 ) ) )
12 9 11 mpbird ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) → 𝐹 ∈ ≤𝑂(1) )