Metamath Proof Explorer

Theorem rnmptbdd

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

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

Proof

Step Hyp Ref Expression
1 rnmptbdd.x ⊢ Ⅎ x φ
2 rnmptbdd.b ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
3 breq2 ⊢ y = v → B ≤ y ↔ B ≤ v
4 3 ralbidv ⊢ y = v → ∀ x ∈ A B ≤ y ↔ ∀ x ∈ A B ≤ v
5 4 cbvrexvw ⊢ ∃ y ∈ ℝ ∀ x ∈ A B ≤ y ↔ ∃ v ∈ ℝ ∀ x ∈ A B ≤ v
6 2 5 sylib ⊢ φ → ∃ v ∈ ℝ ∀ x ∈ A B ≤ v
7 1 6 rnmptbddlem ⊢ φ → ∃ v ∈ ℝ ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ v
8 breq2 ⊢ v = y → w ≤ v ↔ w ≤ y
9 8 ralbidv ⊢ v = y → ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ v ↔ ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ y
10 breq1 ⊢ w = z → w ≤ y ↔ z ≤ y
11 10 cbvralvw ⊢ ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ y ↔ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
12 9 11 bitrdi ⊢ v = y → ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ v ↔ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
13 12 cbvrexvw ⊢ ∃ v ∈ ℝ ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ v ↔ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
14 7 13 sylib ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y