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∈AB≤y
Assertion rnmptbdd ⊢φ→∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y

Proof

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