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∈Ay≤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∈Ay≤x→B≤m
5 rexico ⊢A⊆ℝ∧C∈ℝ→∃y∈C+∞∀x∈Ay≤x→B≤m↔∃y∈ℝ∀x∈Ay≤x→B≤m
6 1 3 5 syl2anc ⊢φ→∃y∈C+∞∀x∈Ay≤x→B≤m↔∃y∈ℝ∀x∈Ay≤x→B≤m
7 6 rexbidv ⊢φ→∃m∈ℝ∃y∈C+∞∀x∈Ay≤x→B≤m↔∃m∈ℝ∃y∈ℝ∀x∈Ay≤x→B≤m
8 rexcom ⊢∃y∈C+∞∃m∈ℝ∀x∈Ay≤x→B≤m↔∃m∈ℝ∃y∈C+∞∀x∈Ay≤x→B≤m
9 rexcom ⊢∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→B≤m↔∃m∈ℝ∃y∈ℝ∀x∈Ay≤x→B≤m
10 7 8 9 3bitr4g ⊢φ→∃y∈C+∞∃m∈ℝ∀x∈Ay≤x→B≤m↔∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→B≤m
11 4 10 bitr4d ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃y∈C+∞∃m∈ℝ∀x∈Ay≤x→B≤m