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

Metamath Proof Explorer

Theorem rnmptbd

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

Ref Expression
Hypotheses rnmptbd.x ⊢ Ⅎ 𝑥 𝜑
rnmptbd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion rnmptbd ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 rnmptbd.x ⊢ Ⅎ 𝑥 𝜑
2 rnmptbd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑤 ) )
4 3 ralbidv ⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) )
5 4 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 )
6 5 a1i ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) )
7 nfv ⊢ Ⅎ 𝑤 𝜑
8 1 7 2 rnmptbdlem ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ) )
9 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑢 ≤ 𝑤 ↔ 𝑢 ≤ 𝑦 ) )
10 9 ralbidv ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑦 ) )
11 breq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦 ) )
12 11 cbvralvw ⊢ ( ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
13 10 12 bitrdi ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
14 13 cbvrexvw ⊢ ( ∃ 𝑤 ∈ ℝ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
15 14 a1i ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
16 6 8 15 3bitrd ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )