Metamath Proof Explorer

Theorem ello1mpt2

Description: 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 ∈ ℝ
Assertion ello1mpt2 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m

Proof

Step Hyp Ref Expression
1 ello1mpt.1 ⊢ φ → A ⊆ ℝ
2 ello1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 ello1d.3 ⊢ φ → C ∈ ℝ
4 1 2 ello1mpt ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
5 rexico ⊢ A ⊆ ℝ ∧ C ∈ ℝ → ∃ y ∈ C +∞ ∀ x ∈ A y ≤ x → B ≤ m ↔ ∃ y ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
6 1 3 5 syl2anc ⊢ φ → ∃ y ∈ C +∞ ∀ x ∈ A y ≤ x → B ≤ m ↔ ∃ y ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
7 6 rexbidv ⊢ φ → ∃ m ∈ ℝ ∃ y ∈ C +∞ ∀ x ∈ A y ≤ x → B ≤ m ↔ ∃ m ∈ ℝ ∃ y ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
8 rexcom ⊢ ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m ↔ ∃ m ∈ ℝ ∃ y ∈ C +∞ ∀ x ∈ A y ≤ x → B ≤ m
9 rexcom ⊢ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m ↔ ∃ m ∈ ℝ ∃ y ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
10 7 8 9 3bitr4g ⊢ φ → ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
11 4 10 bitr4d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m