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