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∈vxball⁡Md=X

Proof

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