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 ∈ X b = x ball ⁡ M d
2 1 simprbi ⊢ M ∈ TotBnd ⁡ X → ∀ d ∈ ℝ + ∃ v ∈ Fin ⋃ v = X ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
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 ∈ X b = x ball ⁡ M d → S ⊆ ⋃ v ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
6 5 reximdv ⊢ S ⊆ X → ∃ v ∈ Fin ⋃ v = X ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d → ∃ v ∈ Fin S ⊆ ⋃ v ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
7 6 ralimdv ⊢ S ⊆ X → ∀ d ∈ ℝ + ∃ v ∈ Fin ⋃ v = X ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d → ∀ d ∈ ℝ + ∃ v ∈ Fin S ⊆ ⋃ v ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
8 2 7 mpan9 ⊢ M ∈ TotBnd ⁡ X ∧ S ⊆ X → ∀ d ∈ ℝ + ∃ v ∈ Fin S ⊆ ⋃ v ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
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 ∈ Fin S ⊆ ⋃ v ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
12 9 11 sylan ⊢ M ∈ TotBnd ⁡ X ∧ S ⊆ X → M ↾ S × S ∈ TotBnd ⁡ S ↔ ∀ d ∈ ℝ + ∃ v ∈ Fin S ⊆ ⋃ v ∧ ∀ b ∈ v ∃ x ∈ X b = x ball ⁡ M d
13 8 12 mpbird ⊢ M ∈ TotBnd ⁡ X ∧ S ⊆ X → M ↾ S × S ∈ TotBnd ⁡ S