Metamath Proof Explorer

Theorem ello1mpt

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 ∈ ℝ
Assertion ello1mpt ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m

Proof

Step Hyp Ref Expression
1 ello1mpt.1 ⊢ φ → A ⊆ ℝ
2 ello1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 2 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ ℝ
4 ello12 ⊢ x ∈ A ⟼ B : A ⟶ ℝ ∧ A ⊆ ℝ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ z ∈ A y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m
5 3 1 4 syl2anc ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ z ∈ A y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m
6 nfv ⊢ Ⅎ x y ≤ z
7 nffvmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B ⁡ z
8 nfcv ⊢ Ⅎ _ x ≤
9 nfcv ⊢ Ⅎ _ x m
10 7 8 9 nfbr ⊢ Ⅎ x x ∈ A ⟼ B ⁡ z ≤ m
11 6 10 nfim ⊢ Ⅎ x y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m
12 nfv ⊢ Ⅎ z y ≤ x → x ∈ A ⟼ B ⁡ x ≤ m
13 breq2 ⊢ z = x → y ≤ z ↔ y ≤ x
14 fveq2 ⊢ z = x → x ∈ A ⟼ B ⁡ z = x ∈ A ⟼ B ⁡ x
15 14 breq1d ⊢ z = x → x ∈ A ⟼ B ⁡ z ≤ m ↔ x ∈ A ⟼ B ⁡ x ≤ m
16 13 15 imbi12d ⊢ z = x → y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m ↔ y ≤ x → x ∈ A ⟼ B ⁡ x ≤ m
17 11 12 16 cbvralw ⊢ ∀ z ∈ A y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m ↔ ∀ x ∈ A y ≤ x → x ∈ A ⟼ B ⁡ x ≤ m
18 simpr ⊢ φ ∧ x ∈ A → x ∈ A
19 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
20 19 fvmpt2 ⊢ x ∈ A ∧ B ∈ ℝ → x ∈ A ⟼ B ⁡ x = B
21 18 2 20 syl2anc ⊢ φ ∧ x ∈ A → x ∈ A ⟼ B ⁡ x = B
22 21 breq1d ⊢ φ ∧ x ∈ A → x ∈ A ⟼ B ⁡ x ≤ m ↔ B ≤ m
23 22 imbi2d ⊢ φ ∧ x ∈ A → y ≤ x → x ∈ A ⟼ B ⁡ x ≤ m ↔ y ≤ x → B ≤ m
24 23 ralbidva ⊢ φ → ∀ x ∈ A y ≤ x → x ∈ A ⟼ B ⁡ x ≤ m ↔ ∀ x ∈ A y ≤ x → B ≤ m
25 17 24 syl5bb ⊢ φ → ∀ z ∈ A y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m ↔ ∀ x ∈ A y ≤ x → B ≤ m
26 25 2rexbidv ⊢ φ → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ z ∈ A y ≤ z → x ∈ A ⟼ B ⁡ z ≤ m ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
27 5 26 bitrd ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m