This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )