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 ⊢ M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∃ x ∈ ℝ ∀ y ∈ X ∀ z ∈ X y M z ≤ x

Proof

Step Hyp Ref Expression
1 isbnd3 ⊢ M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∃ x ∈ ℝ M : X × X ⟶ 0 x
2 metf ⊢ M ∈ Met ⁡ X → M : X × X ⟶ ℝ
3 2 adantr ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ → M : X × X ⟶ ℝ
4 ffn ⊢ M : X × X ⟶ ℝ → M Fn X × X
5 ffnov ⊢ M : X × X ⟶ 0 x ↔ M Fn X × X ∧ ∀ y ∈ X ∀ z ∈ X y M z ∈ 0 x
6 5 baib ⊢ M Fn X × X → M : X × X ⟶ 0 x ↔ ∀ y ∈ X ∀ z ∈ X y M z ∈ 0 x
7 3 4 6 3syl ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ → M : X × X ⟶ 0 x ↔ ∀ y ∈ X ∀ z ∈ X y M z ∈ 0 x
8 0red ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ ∧ y ∈ X ∧ z ∈ X → 0 ∈ ℝ
9 simplr ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ ∧ y ∈ X ∧ z ∈ X → x ∈ ℝ
10 metcl ⊢ M ∈ Met ⁡ X ∧ y ∈ X ∧ z ∈ X → y M z ∈ ℝ
11 10 3expb ⊢ M ∈ Met ⁡ X ∧ y ∈ X ∧ z ∈ X → y M z ∈ ℝ
12 11 adantlr ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ ∧ y ∈ X ∧ z ∈ X → y M z ∈ ℝ
13 metge0 ⊢ M ∈ Met ⁡ X ∧ y ∈ X ∧ z ∈ X → 0 ≤ y M z
14 13 3expb ⊢ M ∈ Met ⁡ X ∧ y ∈ X ∧ z ∈ X → 0 ≤ y M z
15 14 adantlr ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ ∧ y ∈ X ∧ z ∈ X → 0 ≤ y M z
16 elicc2 ⊢ 0 ∈ ℝ ∧ x ∈ ℝ → y M z ∈ 0 x ↔ y M z ∈ ℝ ∧ 0 ≤ y M z ∧ y M z ≤ x
17 df-3an ⊢ y M z ∈ ℝ ∧ 0 ≤ y M z ∧ y M z ≤ x ↔ y M z ∈ ℝ ∧ 0 ≤ y M z ∧ y M z ≤ x
18 16 17 syl6bb ⊢ 0 ∈ ℝ ∧ x ∈ ℝ → y M z ∈ 0 x ↔ y M z ∈ ℝ ∧ 0 ≤ y M z ∧ y M z ≤ x
19 18 baibd ⊢ 0 ∈ ℝ ∧ x ∈ ℝ ∧ y M z ∈ ℝ ∧ 0 ≤ y M z → y M z ∈ 0 x ↔ y M z ≤ x
20 8 9 12 15 19 syl22anc ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ ∧ y ∈ X ∧ z ∈ X → y M z ∈ 0 x ↔ y M z ≤ x
21 20 2ralbidva ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ → ∀ y ∈ X ∀ z ∈ X y M z ∈ 0 x ↔ ∀ y ∈ X ∀ z ∈ X y M z ≤ x
22 7 21 bitrd ⊢ M ∈ Met ⁡ X ∧ x ∈ ℝ → M : X × X ⟶ 0 x ↔ ∀ y ∈ X ∀ z ∈ X y M z ≤ x
23 22 rexbidva ⊢ M ∈ Met ⁡ X → ∃ x ∈ ℝ M : X × X ⟶ 0 x ↔ ∃ x ∈ ℝ ∀ y ∈ X ∀ z ∈ X y M z ≤ x
24 23 pm5.32i ⊢ M ∈ Met ⁡ X ∧ ∃ x ∈ ℝ M : X × X ⟶ 0 x ↔ M ∈ Met ⁡ X ∧ ∃ x ∈ ℝ ∀ y ∈ X ∀ z ∈ X y M z ≤ x
25 1 24 bitri ⊢ M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∃ x ∈ ℝ ∀ y ∈ X ∀ z ∈ X y M z ≤ x