Metamath Proof Explorer


Theorem isbnd

Description: The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion isbnd M Bnd X M Met X x X r + X = x ball M r

Proof

Step Hyp Ref Expression
1 elfvex M Bnd X X V
2 elfvex M Met X X V
3 2 adantr M Met X x X r + X = x ball M r X V
4 fveq2 y = X Met y = Met X
5 eqeq1 y = X y = x ball m r X = x ball m r
6 5 rexbidv y = X r + y = x ball m r r + X = x ball m r
7 6 raleqbi1dv y = X x y r + y = x ball m r x X r + X = x ball m r
8 4 7 rabeqbidv y = X m Met y | x y r + y = x ball m r = m Met X | x X r + X = x ball m r
9 df-bnd Bnd = y V m Met y | x y r + y = x ball m r
10 fvex Met X V
11 10 rabex m Met X | x X r + X = x ball m r V
12 8 9 11 fvmpt X V Bnd X = m Met X | x X r + X = x ball m r
13 12 eleq2d X V M Bnd X M m Met X | x X r + X = x ball m r
14 fveq2 m = M ball m = ball M
15 14 oveqd m = M x ball m r = x ball M r
16 15 eqeq2d m = M X = x ball m r X = x ball M r
17 16 rexbidv m = M r + X = x ball m r r + X = x ball M r
18 17 ralbidv m = M x X r + X = x ball m r x X r + X = x ball M r
19 18 elrab M m Met X | x X r + X = x ball m r M Met X x X r + X = x ball M r
20 13 19 bitrdi X V M Bnd X M Met X x X r + X = x ball M r
21 1 3 20 pm5.21nii M Bnd X M Met X x X r + X = x ball M r