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