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 ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑀 𝑧 ) ≤ 𝑥 ) )