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

Metamath Proof Explorer

Theorem rnmptbd2

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

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

Proof

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