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 ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )