Metamath Proof Explorer


Theorem isbnd3b

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Assertion isbnd3b ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 isbnd3 ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) )
2 metf ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
3 2 adantr ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
4 ffn ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ → 𝑀 Fn ( 𝑋 × 𝑋 ) )
5 ffnov ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ ( 𝑀 Fn ( 𝑋 × 𝑋 ) ∧ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ) )
6 5 baib ( 𝑀 Fn ( 𝑋 × 𝑋 ) → ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ) )
7 3 4 6 3syl ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ) )
8 0red ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → 0 ∈ ℝ )
9 simplr ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → 𝑥 ∈ ℝ )
10 metcl ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦𝑋𝑧𝑋 ) → ( 𝑦 𝑀 𝑧 ) ∈ ℝ )
11 10 3expb ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → ( 𝑦 𝑀 𝑧 ) ∈ ℝ )
12 11 adantlr ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → ( 𝑦 𝑀 𝑧 ) ∈ ℝ )
13 metge0 ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑦𝑋𝑧𝑋 ) → 0 ≤ ( 𝑦 𝑀 𝑧 ) )
14 13 3expb ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → 0 ≤ ( 𝑦 𝑀 𝑧 ) )
15 14 adantlr ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → 0 ≤ ( 𝑦 𝑀 𝑧 ) )
16 elicc2 ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) ) )
17 df-3an ( ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) ↔ ( ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
18 16 17 bitrdi ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ) ∧ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) ) )
19 18 baibd ( ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝑦 𝑀 𝑧 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 𝑀 𝑧 ) ) ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
20 8 9 12 15 19 syl22anc ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑦𝑋𝑧𝑋 ) ) → ( ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
21 20 2ralbidva ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ∈ ( 0 [,] 𝑥 ) ↔ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
22 7 21 bitrd ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
23 22 rexbidva ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
24 23 pm5.32i ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] 𝑥 ) ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )
25 1 24 bitri ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝑋𝑧𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )