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 ∈ A B ≤ y ↔ ∃ w ∈ ℝ ∀ x ∈ A B ≤ w ∧ ∃ z ∈ ℝ ∀ x ∈ A z ≤ B

Proof

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