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 eqtr3id 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 eqtr3id 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