Metamath Proof Explorer

Theorem rnmptbd2

Description: Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rnmptbd2.x ⊢ Ⅎ x φ
rnmptbd2.b ⊢ φ ∧ x ∈ A → B ∈ V
Assertion rnmptbd2 ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z

Proof

Step Hyp Ref Expression
1 rnmptbd2.x ⊢ Ⅎ x φ
2 rnmptbd2.b ⊢ φ ∧ x ∈ A → B ∈ V
3 breq1 ⊢ y = w → y ≤ B ↔ w ≤ B
4 3 ralbidv ⊢ y = w → ∀ x ∈ A y ≤ B ↔ ∀ x ∈ A w ≤ B
5 4 cbvrexvw ⊢ ∃ y ∈ ℝ ∀ x ∈ A y ≤ B ↔ ∃ w ∈ ℝ ∀ x ∈ A w ≤ B
6 5 a1i ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B ↔ ∃ w ∈ ℝ ∀ x ∈ A w ≤ B
7 1 2 rnmptbd2lem ⊢ φ → ∃ w ∈ ℝ ∀ x ∈ A w ≤ B ↔ ∃ w ∈ ℝ ∀ u ∈ ran ⁡ x ∈ A ⟼ B w ≤ u
8 breq1 ⊢ w = y → w ≤ u ↔ y ≤ u
9 8 ralbidv ⊢ w = y → ∀ u ∈ ran ⁡ x ∈ A ⟼ B w ≤ u ↔ ∀ u ∈ ran ⁡ x ∈ A ⟼ B y ≤ u
10 breq2 ⊢ u = z → y ≤ u ↔ y ≤ z
11 10 cbvralvw ⊢ ∀ u ∈ ran ⁡ x ∈ A ⟼ B y ≤ u ↔ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
12 9 11 syl6bb ⊢ w = y → ∀ u ∈ ran ⁡ x ∈ A ⟼ B w ≤ u ↔ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
13 12 cbvrexvw ⊢ ∃ w ∈ ℝ ∀ u ∈ ran ⁡ x ∈ A ⟼ B w ≤ u ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
14 13 a1i ⊢ φ → ∃ w ∈ ℝ ∀ u ∈ ran ⁡ x ∈ A ⟼ B w ≤ u ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z
15 6 7 14 3bitrd ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A y ≤ B ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z