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 ⊢Ⅎxφ
rexabsle.2 ⊢φ∧x∈A→B∈ℝ
Assertion rexabsle ⊢φ→∃y∈ℝ∀x∈AB≤y↔∃w∈ℝ∀x∈AB≤w∧∃z∈ℝ∀x∈Az≤B

Proof

Step Hyp Ref Expression
1 rexabsle.1 ⊢Ⅎxφ
2 rexabsle.2 ⊢φ∧x∈A→B∈ℝ
3 nfv ⊢Ⅎxy=a
4 breq2 ⊢y=a→B≤y↔B≤a
5 3 4 ralbid ⊢y=a→∀x∈AB≤y↔∀x∈AB≤a
6 5 cbvrexvw ⊢∃y∈ℝ∀x∈AB≤y↔∃a∈ℝ∀x∈AB≤a
7 6 a1i ⊢φ→∃y∈ℝ∀x∈AB≤y↔∃a∈ℝ∀x∈AB≤a
8 1 2 rexabslelem ⊢φ→∃a∈ℝ∀x∈AB≤a↔∃b∈ℝ∀x∈AB≤b∧∃c∈ℝ∀x∈Ac≤B
9 breq2 ⊢b=w→B≤b↔B≤w
10 9 ralbidv ⊢b=w→∀x∈AB≤b↔∀x∈AB≤w
11 10 cbvrexvw ⊢∃b∈ℝ∀x∈AB≤b↔∃w∈ℝ∀x∈AB≤w
12 breq1 ⊢c=z→c≤B↔z≤B
13 12 ralbidv ⊢c=z→∀x∈Ac≤B↔∀x∈Az≤B
14 13 cbvrexvw ⊢∃c∈ℝ∀x∈Ac≤B↔∃z∈ℝ∀x∈Az≤B
15 11 14 anbi12i ⊢∃b∈ℝ∀x∈AB≤b∧∃c∈ℝ∀x∈Ac≤B↔∃w∈ℝ∀x∈AB≤w∧∃z∈ℝ∀x∈Az≤B
16 15 a1i ⊢φ→∃b∈ℝ∀x∈AB≤b∧∃c∈ℝ∀x∈Ac≤B↔∃w∈ℝ∀x∈AB≤w∧∃z∈ℝ∀x∈Az≤B
17 7 8 16 3bitrd ⊢φ→∃y∈ℝ∀x∈AB≤y↔∃w∈ℝ∀x∈AB≤w∧∃z∈ℝ∀x∈Az≤B