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

Metamath Proof Explorer

Theorem ello1d

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

Ref Expression
Hypotheses ello1mpt.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ello1mpt.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
ello1d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
ello1d.4 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
ello1d.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ≤ 𝑀 )
Assertion ello1d ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 ello1mpt.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ello1mpt.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 ello1d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 ello1d.4 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
5 ello1d.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ≤ 𝑀 )
6 5 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) )
7 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) )
8 breq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 ≤ 𝑥 ↔ 𝐶 ≤ 𝑥 ) )
9 8 imbi1d ⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
10 9 ralbidv ⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
11 breq2 ⊢ ( 𝑚 = 𝑀 → ( 𝐵 ≤ 𝑚 ↔ 𝐵 ≤ 𝑀 ) )
12 11 imbi2d ⊢ ( 𝑚 = 𝑀 → ( ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) ) )
13 12 ralbidv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) ) )
14 10 13 rspc2ev ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → 𝐵 ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
15 3 4 7 14 syl3anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
16 1 2 ello1mpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
17 15 16 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )