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 ∈ X b = x ball ⁡ M d

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