Metamath Proof Explorer


Theorem sstotbnd

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 N = M Y × Y
Assertion sstotbnd M Met X Y X N TotBnd Y d + v Fin Y v b v x X b = x ball M d

Proof

Step Hyp Ref Expression
1 sstotbnd.2 N = M Y × Y
2 1 sstotbnd2 M Met X Y X N TotBnd Y d + u 𝒫 X Fin Y x u x ball M d
3 elfpw u 𝒫 X Fin u X u Fin
4 3 simprbi u 𝒫 X Fin u Fin
5 mptfi u Fin x u x ball M d Fin
6 rnfi x u x ball M d Fin ran x u x ball M d Fin
7 4 5 6 3syl u 𝒫 X Fin ran x u x ball M d Fin
8 7 ad2antrl M Met X Y X u 𝒫 X Fin Y x u x ball M d ran x u x ball M d Fin
9 simprr M Met X Y X u 𝒫 X Fin Y x u x ball M d Y x u x ball M d
10 eqid x u x ball M d = x u x ball M d
11 10 rnmpt ran x u x ball M d = b | x u b = x ball M d
12 3 simplbi u 𝒫 X Fin u X
13 ssrexv u X x u b = x ball M d x X b = x ball M d
14 12 13 syl u 𝒫 X Fin x u b = x ball M d x X b = x ball M d
15 14 ad2antrl M Met X Y X u 𝒫 X Fin Y x u x ball M d x u b = x ball M d x X b = x ball M d
16 15 ss2abdv M Met X Y X u 𝒫 X Fin Y x u x ball M d b | x u b = x ball M d b | x X b = x ball M d
17 11 16 eqsstrid M Met X Y X u 𝒫 X Fin Y x u x ball M d ran x u x ball M d b | x X b = x ball M d
18 unieq v = ran x u x ball M d v = ran x u x ball M d
19 ovex x ball M d V
20 19 dfiun3 x u x ball M d = ran x u x ball M d
21 18 20 syl6eqr v = ran x u x ball M d v = x u x ball M d
22 21 sseq2d v = ran x u x ball M d Y v Y x u x ball M d
23 ssabral v b | x X b = x ball M d b v x X b = x ball M d
24 sseq1 v = ran x u x ball M d v b | x X b = x ball M d ran x u x ball M d b | x X b = x ball M d
25 23 24 bitr3id v = ran x u x ball M d b v x X b = x ball M d ran x u x ball M d b | x X b = x ball M d
26 22 25 anbi12d v = ran x u x ball M d Y v b v x X b = x ball M d Y x u x ball M d ran x u x ball M d b | x X b = x ball M d
27 26 rspcev ran x u x ball M d Fin Y x u x ball M d ran x u x ball M d b | x X b = x ball M d v Fin Y v b v x X b = x ball M d
28 8 9 17 27 syl12anc M Met X Y X u 𝒫 X Fin Y x u x ball M d v Fin Y v b v x X b = x ball M d
29 28 rexlimdvaa M Met X Y X u 𝒫 X Fin Y x u x ball M d v Fin Y v b v x X b = x ball M d
30 oveq1 x = f b x ball M d = f b ball M d
31 30 eqeq2d x = f b b = x ball M d b = f b ball M d
32 31 ac6sfi v Fin b v x X b = x ball M d f f : v X b v b = f b ball M d
33 32 adantrl v Fin Y v b v x X b = x ball M d f f : v X b v b = f b ball M d
34 33 adantl M Met X Y X v Fin Y v b v x X b = x ball M d f f : v X b v b = f b ball M d
35 frn f : v X ran f X
36 35 ad2antrl M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d ran f X
37 simplrl M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d v Fin
38 ffn f : v X f Fn v
39 38 ad2antrl M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d f Fn v
40 dffn4 f Fn v f : v onto ran f
41 39 40 sylib M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d f : v onto ran f
42 fofi v Fin f : v onto ran f ran f Fin
43 37 41 42 syl2anc M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d ran f Fin
44 elfpw ran f 𝒫 X Fin ran f X ran f Fin
45 36 43 44 sylanbrc M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d ran f 𝒫 X Fin
46 simprrl M Met X Y X v Fin Y v b v x X b = x ball M d Y v
47 46 adantr M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d Y v
48 uniiun v = b v b
49 iuneq2 b v b = f b ball M d b v b = b v f b ball M d
50 48 49 syl5eq b v b = f b ball M d v = b v f b ball M d
51 50 ad2antll M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d v = b v f b ball M d
52 47 51 sseqtrd M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d Y b v f b ball M d
53 30 eleq2d x = f b y x ball M d y f b ball M d
54 53 rexrn f Fn v x ran f y x ball M d b v y f b ball M d
55 eliun y x ran f x ball M d x ran f y x ball M d
56 eliun y b v f b ball M d b v y f b ball M d
57 54 55 56 3bitr4g f Fn v y x ran f x ball M d y b v f b ball M d
58 57 eqrdv f Fn v x ran f x ball M d = b v f b ball M d
59 39 58 syl M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d x ran f x ball M d = b v f b ball M d
60 52 59 sseqtrrd M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d Y x ran f x ball M d
61 iuneq1 u = ran f x u x ball M d = x ran f x ball M d
62 61 sseq2d u = ran f Y x u x ball M d Y x ran f x ball M d
63 62 rspcev ran f 𝒫 X Fin Y x ran f x ball M d u 𝒫 X Fin Y x u x ball M d
64 45 60 63 syl2anc M Met X Y X v Fin Y v b v x X b = x ball M d f : v X b v b = f b ball M d u 𝒫 X Fin Y x u x ball M d
65 34 64 exlimddv M Met X Y X v Fin Y v b v x X b = x ball M d u 𝒫 X Fin Y x u x ball M d
66 65 rexlimdvaa M Met X Y X v Fin Y v b v x X b = x ball M d u 𝒫 X Fin Y x u x ball M d
67 29 66 impbid M Met X Y X u 𝒫 X Fin Y x u x ball M d v Fin Y v b v x X b = x ball M d
68 67 ralbidv M Met X Y X d + u 𝒫 X Fin Y x u x ball M d d + v Fin Y v b v x X b = x ball M d
69 2 68 bitrd M Met X Y X N TotBnd Y d + v Fin Y v b v x X b = x ball M d