Metamath Proof Explorer

Theorem isbnd

Description: The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbnd ⊢ M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ M r

Proof

Step Hyp Ref Expression
1 elfvex ⊢ M ∈ Bnd ⁡ X → X ∈ V
2 elfvex ⊢ M ∈ Met ⁡ X → X ∈ V
3 2 adantr ⊢ M ∈ Met ⁡ X ∧ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ M r → X ∈ V
4 fveq2 ⊢ y = X → Met ⁡ y = Met ⁡ X
5 eqeq1 ⊢ y = X → y = x ball ⁡ m r ↔ X = x ball ⁡ m r
6 5 rexbidv ⊢ y = X → ∃ r ∈ ℝ + y = x ball ⁡ m r ↔ ∃ r ∈ ℝ + X = x ball ⁡ m r
7 6 raleqbi1dv ⊢ y = X → ∀ x ∈ y ∃ r ∈ ℝ + y = x ball ⁡ m r ↔ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r
8 4 7 rabeqbidv ⊢ y = X → m ∈ Met ⁡ y | ∀ x ∈ y ∃ r ∈ ℝ + y = x ball ⁡ m r = m ∈ Met ⁡ X | ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r
9 df-bnd ⊢ Bnd = y ∈ V ⟼ m ∈ Met ⁡ y | ∀ x ∈ y ∃ r ∈ ℝ + y = x ball ⁡ m r
10 fvex ⊢ Met ⁡ X ∈ V
11 10 rabex ⊢ m ∈ Met ⁡ X | ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r ∈ V
12 8 9 11 fvmpt ⊢ X ∈ V → Bnd ⁡ X = m ∈ Met ⁡ X | ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r
13 12 eleq2d ⊢ X ∈ V → M ∈ Bnd ⁡ X ↔ M ∈ m ∈ Met ⁡ X | ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r
14 fveq2 ⊢ m = M → ball ⁡ m = ball ⁡ M
15 14 oveqd ⊢ m = M → x ball ⁡ m r = x ball ⁡ M r
16 15 eqeq2d ⊢ m = M → X = x ball ⁡ m r ↔ X = x ball ⁡ M r
17 16 rexbidv ⊢ m = M → ∃ r ∈ ℝ + X = x ball ⁡ m r ↔ ∃ r ∈ ℝ + X = x ball ⁡ M r
18 17 ralbidv ⊢ m = M → ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r ↔ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ M r
19 18 elrab ⊢ M ∈ m ∈ Met ⁡ X | ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ m r ↔ M ∈ Met ⁡ X ∧ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ M r
20 13 19 bitrdi ⊢ X ∈ V → M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ M r
21 1 3 20 pm5.21nii ⊢ M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ x ∈ X ∃ r ∈ ℝ + X = x ball ⁡ M r