Metamath Proof Explorer

Theorem totbndss

Description: A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion totbndss ⊢M∈TotBnd⁡X∧S⊆X→M↾S×S∈TotBnd⁡S

Proof

Step Hyp Ref Expression
1 istotbnd ⊢M∈TotBnd⁡X↔M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
2 1 simprbi ⊢M∈TotBnd⁡X→∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
3 sseq2 ⊢⋃v=X→S⊆⋃v↔S⊆X
4 3 biimprcd ⊢S⊆X→⋃v=X→S⊆⋃v
5 4 anim1d ⊢S⊆X→⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md→S⊆⋃v∧∀b∈v∃x∈Xb=xball⁡Md
6 5 reximdv ⊢S⊆X→∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md→∃v∈FinS⊆⋃v∧∀b∈v∃x∈Xb=xball⁡Md
7 6 ralimdv ⊢S⊆X→∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md→∀d∈ℝ+∃v∈FinS⊆⋃v∧∀b∈v∃x∈Xb=xball⁡Md
8 2 7 mpan9 ⊢M∈TotBnd⁡X∧S⊆X→∀d∈ℝ+∃v∈FinS⊆⋃v∧∀b∈v∃x∈Xb=xball⁡Md
9 totbndmet ⊢M∈TotBnd⁡X→M∈Met⁡X
10 eqid ⊢M↾S×S=M↾S×S
11 10 sstotbnd ⊢M∈Met⁡X∧S⊆X→M↾S×S∈TotBnd⁡S↔∀d∈ℝ+∃v∈FinS⊆⋃v∧∀b∈v∃x∈Xb=xball⁡Md
12 9 11 sylan ⊢M∈TotBnd⁡X∧S⊆X→M↾S×S∈TotBnd⁡S↔∀d∈ℝ+∃v∈FinS⊆⋃v∧∀b∈v∃x∈Xb=xball⁡Md
13 8 12 mpbird ⊢M∈TotBnd⁡X∧S⊆X→M↾S×S∈TotBnd⁡S