Metamath Proof Explorer

Theorem istotbnd3

Description: A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion istotbnd3 ⊢ M ∈ TotBnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ d ∈ ℝ + ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X

Proof

Step Hyp Ref Expression
1 istotbnd ⊢ M ∈ TotBnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ d ∈ ℝ + ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d
2 oveq1 ⊢ x = f ⁡ b → x ball ⁡ M d = f ⁡ b ball ⁡ M d
3 2 eqeq2d ⊢ x = f ⁡ b → b = x ball ⁡ M d ↔ b = f ⁡ b ball ⁡ M d
4 3 ac6sfi ⊢ w ∈ Fin ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d → ∃ f f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d
5 4 ex ⊢ w ∈ Fin → ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d → ∃ f f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d
6 5 ad2antlr ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X → ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d → ∃ f f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d
7 simprrl ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → f : w ⟶ X
8 7 frnd ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ran ⁡ f ⊆ X
9 simplr ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → w ∈ Fin
10 7 ffnd ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → f Fn w
11 dffn4 ⊢ f Fn w ↔ f : w ⟶ onto ran ⁡ f
12 10 11 sylib ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → f : w ⟶ onto ran ⁡ f
13 fofi ⊢ w ∈ Fin ∧ f : w ⟶ onto ran ⁡ f → ran ⁡ f ∈ Fin
14 9 12 13 syl2anc ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ran ⁡ f ∈ Fin
15 elfpw ⊢ ran ⁡ f ∈ 𝒫 X ∩ Fin ↔ ran ⁡ f ⊆ X ∧ ran ⁡ f ∈ Fin
16 8 14 15 sylanbrc ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ran ⁡ f ∈ 𝒫 X ∩ Fin
17 2 eleq2d ⊢ x = f ⁡ b → v ∈ x ball ⁡ M d ↔ v ∈ f ⁡ b ball ⁡ M d
18 17 rexrn ⊢ f Fn w → ∃ x ∈ ran ⁡ f v ∈ x ball ⁡ M d ↔ ∃ b ∈ w v ∈ f ⁡ b ball ⁡ M d
19 10 18 syl ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ∃ x ∈ ran ⁡ f v ∈ x ball ⁡ M d ↔ ∃ b ∈ w v ∈ f ⁡ b ball ⁡ M d
20 eliun ⊢ v ∈ ⋃ x ∈ ran ⁡ f x ball ⁡ M d ↔ ∃ x ∈ ran ⁡ f v ∈ x ball ⁡ M d
21 eliun ⊢ v ∈ ⋃ b ∈ w f ⁡ b ball ⁡ M d ↔ ∃ b ∈ w v ∈ f ⁡ b ball ⁡ M d
22 19 20 21 3bitr4g ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → v ∈ ⋃ x ∈ ran ⁡ f x ball ⁡ M d ↔ v ∈ ⋃ b ∈ w f ⁡ b ball ⁡ M d
23 22 eqrdv ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ⋃ x ∈ ran ⁡ f x ball ⁡ M d = ⋃ b ∈ w f ⁡ b ball ⁡ M d
24 simprrr ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ∀ b ∈ w b = f ⁡ b ball ⁡ M d
25 iuneq2 ⊢ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ⋃ b ∈ w b = ⋃ b ∈ w f ⁡ b ball ⁡ M d
26 24 25 syl ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ⋃ b ∈ w b = ⋃ b ∈ w f ⁡ b ball ⁡ M d
27 uniiun ⊢ ⋃ w = ⋃ b ∈ w b
28 simprl ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ⋃ w = X
29 27 28 syl5eqr ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ⋃ b ∈ w b = X
30 23 26 29 3eqtr2d ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ⋃ x ∈ ran ⁡ f x ball ⁡ M d = X
31 iuneq1 ⊢ v = ran ⁡ f → ⋃ x ∈ v x ball ⁡ M d = ⋃ x ∈ ran ⁡ f x ball ⁡ M d
32 31 eqeq1d ⊢ v = ran ⁡ f → ⋃ x ∈ v x ball ⁡ M d = X ↔ ⋃ x ∈ ran ⁡ f x ball ⁡ M d = X
33 32 rspcev ⊢ ran ⁡ f ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ ran ⁡ f x ball ⁡ M d = X → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
34 16 30 33 syl2anc ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X ∧ f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
35 34 expr ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X → f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
36 35 exlimdv ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X → ∃ f f : w ⟶ X ∧ ∀ b ∈ w b = f ⁡ b ball ⁡ M d → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
37 6 36 syld ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin ∧ ⋃ w = X → ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
38 37 expimpd ⊢ M ∈ Met ⁡ X ∧ w ∈ Fin → ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
39 38 rexlimdva ⊢ M ∈ Met ⁡ X → ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
40 elfpw ⊢ v ∈ 𝒫 X ∩ Fin ↔ v ⊆ X ∧ v ∈ Fin
41 40 simprbi ⊢ v ∈ 𝒫 X ∩ Fin → v ∈ Fin
42 41 ad2antrl ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → v ∈ Fin
43 mptfi ⊢ v ∈ Fin → x ∈ v ⟼ x ball ⁡ M d ∈ Fin
44 rnfi ⊢ x ∈ v ⟼ x ball ⁡ M d ∈ Fin → ran ⁡ x ∈ v ⟼ x ball ⁡ M d ∈ Fin
45 42 43 44 3syl ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → ran ⁡ x ∈ v ⟼ x ball ⁡ M d ∈ Fin
46 ovex ⊢ x ball ⁡ M d ∈ V
47 46 dfiun3 ⊢ ⋃ x ∈ v x ball ⁡ M d = ⋃ ran ⁡ x ∈ v ⟼ x ball ⁡ M d
48 simprr ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → ⋃ x ∈ v x ball ⁡ M d = X
49 47 48 syl5eqr ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → ⋃ ran ⁡ x ∈ v ⟼ x ball ⁡ M d = X
50 eqid ⊢ x ∈ v ⟼ x ball ⁡ M d = x ∈ v ⟼ x ball ⁡ M d
51 50 rnmpt ⊢ ran ⁡ x ∈ v ⟼ x ball ⁡ M d = b | ∃ x ∈ v b = x ball ⁡ M d
52 40 simplbi ⊢ v ∈ 𝒫 X ∩ Fin → v ⊆ X
53 52 ad2antrl ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → v ⊆ X
54 ssrexv ⊢ v ⊆ X → ∃ x ∈ v b = x ball ⁡ M d → ∃ x ∈ X b = x ball ⁡ M d
55 53 54 syl ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → ∃ x ∈ v b = x ball ⁡ M d → ∃ x ∈ X b = x ball ⁡ M d
56 55 ss2abdv ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → b | ∃ x ∈ v b = x ball ⁡ M d ⊆ b | ∃ x ∈ X b = x ball ⁡ M d
57 51 56 eqsstrid ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → ran ⁡ x ∈ v ⟼ x ball ⁡ M d ⊆ b | ∃ x ∈ X b = x ball ⁡ M d
58 unieq ⊢ w = ran ⁡ x ∈ v ⟼ x ball ⁡ M d → ⋃ w = ⋃ ran ⁡ x ∈ v ⟼ x ball ⁡ M d
59 58 eqeq1d ⊢ w = ran ⁡ x ∈ v ⟼ x ball ⁡ M d → ⋃ w = X ↔ ⋃ ran ⁡ x ∈ v ⟼ x ball ⁡ M d = X
60 ssabral ⊢ w ⊆ b | ∃ x ∈ X b = x ball ⁡ M d ↔ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d
61 sseq1 ⊢ w = ran ⁡ x ∈ v ⟼ x ball ⁡ M d → w ⊆ b | ∃ x ∈ X b = x ball ⁡ M d ↔ ran ⁡ x ∈ v ⟼ x ball ⁡ M d ⊆ b | ∃ x ∈ X b = x ball ⁡ M d
62 60 61 bitr3id ⊢ w = ran ⁡ x ∈ v ⟼ x ball ⁡ M d → ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d ↔ ran ⁡ x ∈ v ⟼ x ball ⁡ M d ⊆ b | ∃ x ∈ X b = x ball ⁡ M d
63 59 62 anbi12d ⊢ w = ran ⁡ x ∈ v ⟼ x ball ⁡ M d → ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d ↔ ⋃ ran ⁡ x ∈ v ⟼ x ball ⁡ M d = X ∧ ran ⁡ x ∈ v ⟼ x ball ⁡ M d ⊆ b | ∃ x ∈ X b = x ball ⁡ M d
64 63 rspcev ⊢ ran ⁡ x ∈ v ⟼ x ball ⁡ M d ∈ Fin ∧ ⋃ ran ⁡ x ∈ v ⟼ x ball ⁡ M d = X ∧ ran ⁡ x ∈ v ⟼ x ball ⁡ M d ⊆ b | ∃ x ∈ X b = x ball ⁡ M d → ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d
65 45 49 57 64 syl12anc ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin ∧ ⋃ x ∈ v x ball ⁡ M d = X → ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d
66 65 expr ⊢ M ∈ Met ⁡ X ∧ v ∈ 𝒫 X ∩ Fin → ⋃ x ∈ v x ball ⁡ M d = X → ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d
67 66 rexlimdva ⊢ M ∈ Met ⁡ X → ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X → ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d
68 39 67 impbid ⊢ M ∈ Met ⁡ X → ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d ↔ ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
69 68 ralbidv ⊢ M ∈ Met ⁡ X → ∀ d ∈ ℝ + ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d ↔ ∀ d ∈ ℝ + ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
70 69 pm5.32i ⊢ M ∈ Met ⁡ X ∧ ∀ d ∈ ℝ + ∃ w ∈ Fin ⋃ w = X ∧ ∀ b ∈ w ∃ x ∈ X b = x ball ⁡ M d ↔ M ∈ Met ⁡ X ∧ ∀ d ∈ ℝ + ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X
71 1 70 bitri ⊢ M ∈ TotBnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ d ∈ ℝ + ∃ v ∈ 𝒫 X ∩ Fin ⋃ x ∈ v x ball ⁡ M d = X