Metamath Proof Explorer

Theorem istotbnd

Description: The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion istotbnd ⊢M∈TotBnd⁡X↔M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md

Proof

Step Hyp Ref Expression
1 elfvex ⊢M∈TotBnd⁡X→X∈V
2 elfvex ⊢M∈Met⁡X→X∈V
3 2 adantr ⊢M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md→X∈V
4 fveq2 ⊢y=X→Met⁡y=Met⁡X
5 eqeq2 ⊢y=X→⋃v=y↔⋃v=X
6 rexeq ⊢y=X→∃x∈yb=xball⁡md↔∃x∈Xb=xball⁡md
7 6 ralbidv ⊢y=X→∀b∈v∃x∈yb=xball⁡md↔∀b∈v∃x∈Xb=xball⁡md
8 5 7 anbi12d ⊢y=X→⋃v=y∧∀b∈v∃x∈yb=xball⁡md↔⋃v=X∧∀b∈v∃x∈Xb=xball⁡md
9 8 rexbidv ⊢y=X→∃v∈Fin⋃v=y∧∀b∈v∃x∈yb=xball⁡md↔∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md
10 9 ralbidv ⊢y=X→∀d∈ℝ+∃v∈Fin⋃v=y∧∀b∈v∃x∈yb=xball⁡md↔∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md
11 4 10 rabeqbidv ⊢y=X→m∈Met⁡y|∀d∈ℝ+∃v∈Fin⋃v=y∧∀b∈v∃x∈yb=xball⁡md=m∈Met⁡X|∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md
12 df-totbnd ⊢TotBnd=y∈V⟼m∈Met⁡y|∀d∈ℝ+∃v∈Fin⋃v=y∧∀b∈v∃x∈yb=xball⁡md
13 fvex ⊢Met⁡X∈V
14 13 rabex ⊢m∈Met⁡X|∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md∈V
15 11 12 14 fvmpt ⊢X∈V→TotBnd⁡X=m∈Met⁡X|∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md
16 15 eleq2d ⊢X∈V→M∈TotBnd⁡X↔M∈m∈Met⁡X|∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md
17 fveq2 ⊢m=M→ball⁡m=ball⁡M
18 17 oveqd ⊢m=M→xball⁡md=xball⁡Md
19 18 eqeq2d ⊢m=M→b=xball⁡md↔b=xball⁡Md
20 19 rexbidv ⊢m=M→∃x∈Xb=xball⁡md↔∃x∈Xb=xball⁡Md
21 20 ralbidv ⊢m=M→∀b∈v∃x∈Xb=xball⁡md↔∀b∈v∃x∈Xb=xball⁡Md
22 21 anbi2d ⊢m=M→⋃v=X∧∀b∈v∃x∈Xb=xball⁡md↔⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
23 22 rexbidv ⊢m=M→∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md↔∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
24 23 ralbidv ⊢m=M→∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md↔∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
25 24 elrab ⊢M∈m∈Met⁡X|∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡md↔M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
26 16 25 bitrdi ⊢X∈V→M∈TotBnd⁡X↔M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
27 1 3 26 pm5.21nii ⊢M∈TotBnd⁡X↔M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md