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

Metamath Proof Explorer

Theorem rexabsle

Description: An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rexabsle.1 ⊢ Ⅎ 𝑥 𝜑
rexabsle.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion rexabsle ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rexabsle.1 ⊢ Ⅎ 𝑥 𝜑
2 rexabsle.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 nfv ⊢ Ⅎ 𝑥 𝑦 = 𝑎
4 breq2 ⊢ ( 𝑦 = 𝑎 → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( abs ‘ 𝐵 ) ≤ 𝑎 ) )
5 3 4 ralbid ⊢ ( 𝑦 = 𝑎 → ( ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑎 ) )
6 5 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑎 )
7 6 a1i ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑎 ) )
8 1 2 rexabslelem ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑎 ↔ ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑏 ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑐 ≤ 𝐵 ) ) )
9 breq2 ⊢ ( 𝑏 = 𝑤 → ( 𝐵 ≤ 𝑏 ↔ 𝐵 ≤ 𝑤 ) )
10 9 ralbidv ⊢ ( 𝑏 = 𝑤 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑏 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) )
11 10 cbvrexvw ⊢ ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑏 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 )
12 breq1 ⊢ ( 𝑐 = 𝑧 → ( 𝑐 ≤ 𝐵 ↔ 𝑧 ≤ 𝐵 ) )
13 12 ralbidv ⊢ ( 𝑐 = 𝑧 → ( ∀ 𝑥 ∈ 𝐴 𝑐 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) )
14 13 cbvrexvw ⊢ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑐 ≤ 𝐵 ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 )
15 11 14 anbi12i ⊢ ( ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑏 ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑐 ≤ 𝐵 ) ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) )
16 15 a1i ⊢ ( 𝜑 → ( ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑏 ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑐 ≤ 𝐵 ) ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )
17 7 8 16 3bitrd ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )