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 ⊢ φ → A ⊆ ℝ
ello1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
ello1d.3 ⊢ φ → C ∈ ℝ
ello1d.4 ⊢ φ → M ∈ ℝ
ello1d.5 ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ≤ M
Assertion ello1d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 ello1mpt.1 ⊢ φ → A ⊆ ℝ
2 ello1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 ello1d.3 ⊢ φ → C ∈ ℝ
4 ello1d.4 ⊢ φ → M ∈ ℝ
5 ello1d.5 ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ≤ M
6 5 expr ⊢ φ ∧ x ∈ A → C ≤ x → B ≤ M
7 6 ralrimiva ⊢ φ → ∀ x ∈ A C ≤ x → B ≤ M
8 breq1 ⊢ y = C → y ≤ x ↔ C ≤ x
9 8 imbi1d ⊢ y = C → y ≤ x → B ≤ m ↔ C ≤ x → B ≤ m
10 9 ralbidv ⊢ y = C → ∀ x ∈ A y ≤ x → B ≤ m ↔ ∀ x ∈ A C ≤ x → B ≤ m
11 breq2 ⊢ m = M → B ≤ m ↔ B ≤ M
12 11 imbi2d ⊢ m = M → C ≤ x → B ≤ m ↔ C ≤ x → B ≤ M
13 12 ralbidv ⊢ m = M → ∀ x ∈ A C ≤ x → B ≤ m ↔ ∀ x ∈ A C ≤ x → B ≤ M
14 10 13 rspc2ev ⊢ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → B ≤ M → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
15 3 4 7 14 syl3anc ⊢ φ → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
16 1 2 ello1mpt ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
17 15 16 mpbird ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1