Metamath Proof Explorer


Theorem bndss

Description: A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion bndss M Bnd X S X M S × S Bnd S

Proof

Step Hyp Ref Expression
1 metres2 M Met X S X M S × S Met S
2 1 adantlr M Met X y X r + X = y ball M r S X M S × S Met S
3 ssel2 S X x S x X
4 3 ancoms x S S X x X
5 oveq1 y = x y ball M r = x ball M r
6 5 eqeq2d y = x X = y ball M r X = x ball M r
7 6 rexbidv y = x r + X = y ball M r r + X = x ball M r
8 7 rspcva x X y X r + X = y ball M r r + X = x ball M r
9 4 8 sylan x S S X y X r + X = y ball M r r + X = x ball M r
10 9 adantlll M Met X x S S X y X r + X = y ball M r r + X = x ball M r
11 dfss S X S = S X
12 11 biimpi S X S = S X
13 incom S X = X S
14 12 13 syl6eq S X S = X S
15 ineq1 X = x ball M r X S = x ball M r S
16 14 15 sylan9eq S X X = x ball M r S = x ball M r S
17 16 adantll M Met X x S S X X = x ball M r S = x ball M r S
18 17 adantlr M Met X x S S X r + X = x ball M r S = x ball M r S
19 eqid M S × S = M S × S
20 19 blssp M Met X S X x S r + x ball M S × S r = x ball M r S
21 20 an4s M Met X x S S X r + x ball M S × S r = x ball M r S
22 21 anassrs M Met X x S S X r + x ball M S × S r = x ball M r S
23 22 adantr M Met X x S S X r + X = x ball M r x ball M S × S r = x ball M r S
24 18 23 eqtr4d M Met X x S S X r + X = x ball M r S = x ball M S × S r
25 24 ex M Met X x S S X r + X = x ball M r S = x ball M S × S r
26 25 reximdva M Met X x S S X r + X = x ball M r r + S = x ball M S × S r
27 26 imp M Met X x S S X r + X = x ball M r r + S = x ball M S × S r
28 10 27 syldan M Met X x S S X y X r + X = y ball M r r + S = x ball M S × S r
29 28 an32s M Met X x S y X r + X = y ball M r S X r + S = x ball M S × S r
30 29 ex M Met X x S y X r + X = y ball M r S X r + S = x ball M S × S r
31 30 an32s M Met X y X r + X = y ball M r x S S X r + S = x ball M S × S r
32 31 imp M Met X y X r + X = y ball M r x S S X r + S = x ball M S × S r
33 32 an32s M Met X y X r + X = y ball M r S X x S r + S = x ball M S × S r
34 33 ralrimiva M Met X y X r + X = y ball M r S X x S r + S = x ball M S × S r
35 2 34 jca M Met X y X r + X = y ball M r S X M S × S Met S x S r + S = x ball M S × S r
36 isbnd M Bnd X M Met X y X r + X = y ball M r
37 36 anbi1i M Bnd X S X M Met X y X r + X = y ball M r S X
38 isbnd M S × S Bnd S M S × S Met S x S r + S = x ball M S × S r
39 35 37 38 3imtr4i M Bnd X S X M S × S Bnd S