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=xball⁡Mr

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