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 𝑥 𝜑
rnmptbdd.b ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 )
Assertion rnmptbdd ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 )

Proof

Step Hyp Ref Expression
1 rnmptbdd.x 𝑥 𝜑
2 rnmptbdd.b ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 )
3 breq2 ( 𝑦 = 𝑣 → ( 𝐵𝑦𝐵𝑣 ) )
4 3 ralbidv ( 𝑦 = 𝑣 → ( ∀ 𝑥𝐴 𝐵𝑦 ↔ ∀ 𝑥𝐴 𝐵𝑣 ) )
5 4 cbvrexvw ( ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 ↔ ∃ 𝑣 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑣 )
6 2 5 sylib ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑣 )
7 1 6 rnmptbddlem ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑣 )
8 breq2 ( 𝑣 = 𝑦 → ( 𝑤𝑣𝑤𝑦 ) )
9 8 ralbidv ( 𝑣 = 𝑦 → ( ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑣 ↔ ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑦 ) )
10 breq1 ( 𝑤 = 𝑧 → ( 𝑤𝑦𝑧𝑦 ) )
11 10 cbvralvw ( ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 )
12 9 11 bitrdi ( 𝑣 = 𝑦 → ( ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑣 ↔ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 ) )
13 12 cbvrexvw ( ∃ 𝑣 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑣 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 )
14 7 13 sylib ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 )