Metamath Proof Explorer


Theorem ssbnd

Description: A subset of a metric space is bounded iff it is contained in a ball around P , for any P in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypothesis ssbnd.2 N = M Y × Y
Assertion ssbnd M Met X P X N Bnd Y d Y P ball M d

Proof

Step Hyp Ref Expression
1 ssbnd.2 N = M Y × Y
2 0re 0
3 2 ne0ii
4 0ss P ball M d
5 sseq1 Y = Y P ball M d P ball M d
6 4 5 mpbiri Y = Y P ball M d
7 6 ralrimivw Y = d Y P ball M d
8 r19.2z d Y P ball M d d Y P ball M d
9 3 7 8 sylancr Y = d Y P ball M d
10 9 a1i M Met X P X N Bnd Y Y = d Y P ball M d
11 isbnd2 N Bnd Y Y N ∞Met Y y Y r + Y = y ball N r
12 simplll M Met X P X N ∞Met Y y Y r + M Met X
13 1 dmeqi dom N = dom M Y × Y
14 dmres dom M Y × Y = Y × Y dom M
15 13 14 eqtri dom N = Y × Y dom M
16 xmetf N ∞Met Y N : Y × Y *
17 16 fdmd N ∞Met Y dom N = Y × Y
18 15 17 syl5eqr N ∞Met Y Y × Y dom M = Y × Y
19 df-ss Y × Y dom M Y × Y dom M = Y × Y
20 18 19 sylibr N ∞Met Y Y × Y dom M
21 20 ad2antlr M Met X P X N ∞Met Y y Y r + Y × Y dom M
22 metf M Met X M : X × X
23 22 fdmd M Met X dom M = X × X
24 23 ad3antrrr M Met X P X N ∞Met Y y Y r + dom M = X × X
25 21 24 sseqtrd M Met X P X N ∞Met Y y Y r + Y × Y X × X
26 dmss Y × Y X × X dom Y × Y dom X × X
27 25 26 syl M Met X P X N ∞Met Y y Y r + dom Y × Y dom X × X
28 dmxpid dom Y × Y = Y
29 dmxpid dom X × X = X
30 27 28 29 3sstr3g M Met X P X N ∞Met Y y Y r + Y X
31 simprl M Met X P X N ∞Met Y y Y r + y Y
32 30 31 sseldd M Met X P X N ∞Met Y y Y r + y X
33 simpllr M Met X P X N ∞Met Y y Y r + P X
34 metcl M Met X y X P X y M P
35 12 32 33 34 syl3anc M Met X P X N ∞Met Y y Y r + y M P
36 rpre r + r
37 36 ad2antll M Met X P X N ∞Met Y y Y r + r
38 35 37 readdcld M Met X P X N ∞Met Y y Y r + y M P + r
39 metxmet M Met X M ∞Met X
40 12 39 syl M Met X P X N ∞Met Y y Y r + M ∞Met X
41 32 31 elind M Met X P X N ∞Met Y y Y r + y X Y
42 rpxr r + r *
43 42 ad2antll M Met X P X N ∞Met Y y Y r + r *
44 1 blres M ∞Met X y X Y r * y ball N r = y ball M r Y
45 40 41 43 44 syl3anc M Met X P X N ∞Met Y y Y r + y ball N r = y ball M r Y
46 inss1 y ball M r Y y ball M r
47 35 leidd M Met X P X N ∞Met Y y Y r + y M P y M P
48 35 recnd M Met X P X N ∞Met Y y Y r + y M P
49 37 recnd M Met X P X N ∞Met Y y Y r + r
50 48 49 pncand M Met X P X N ∞Met Y y Y r + y M P + r - r = y M P
51 47 50 breqtrrd M Met X P X N ∞Met Y y Y r + y M P y M P + r - r
52 blss2 M ∞Met X y X P X r y M P + r y M P y M P + r - r y ball M r P ball M y M P + r
53 40 32 33 37 38 51 52 syl33anc M Met X P X N ∞Met Y y Y r + y ball M r P ball M y M P + r
54 46 53 sstrid M Met X P X N ∞Met Y y Y r + y ball M r Y P ball M y M P + r
55 45 54 eqsstrd M Met X P X N ∞Met Y y Y r + y ball N r P ball M y M P + r
56 oveq2 d = y M P + r P ball M d = P ball M y M P + r
57 56 sseq2d d = y M P + r y ball N r P ball M d y ball N r P ball M y M P + r
58 57 rspcev y M P + r y ball N r P ball M y M P + r d y ball N r P ball M d
59 38 55 58 syl2anc M Met X P X N ∞Met Y y Y r + d y ball N r P ball M d
60 sseq1 Y = y ball N r Y P ball M d y ball N r P ball M d
61 60 rexbidv Y = y ball N r d Y P ball M d d y ball N r P ball M d
62 59 61 syl5ibrcom M Met X P X N ∞Met Y y Y r + Y = y ball N r d Y P ball M d
63 62 rexlimdvva M Met X P X N ∞Met Y y Y r + Y = y ball N r d Y P ball M d
64 63 expimpd M Met X P X N ∞Met Y y Y r + Y = y ball N r d Y P ball M d
65 11 64 syl5bi M Met X P X N Bnd Y Y d Y P ball M d
66 65 expdimp M Met X P X N Bnd Y Y d Y P ball M d
67 10 66 pm2.61dne M Met X P X N Bnd Y d Y P ball M d
68 67 ex M Met X P X N Bnd Y d Y P ball M d
69 simprr M Met X P X d Y P ball M d Y P ball M d
70 xpss12 Y P ball M d Y P ball M d Y × Y P ball M d × P ball M d
71 69 69 70 syl2anc M Met X P X d Y P ball M d Y × Y P ball M d × P ball M d
72 71 resabs1d M Met X P X d Y P ball M d M P ball M d × P ball M d Y × Y = M Y × Y
73 72 1 syl6eqr M Met X P X d Y P ball M d M P ball M d × P ball M d Y × Y = N
74 blbnd M ∞Met X P X d M P ball M d × P ball M d Bnd P ball M d
75 39 74 syl3an1 M Met X P X d M P ball M d × P ball M d Bnd P ball M d
76 75 3expa M Met X P X d M P ball M d × P ball M d Bnd P ball M d
77 76 adantrr M Met X P X d Y P ball M d M P ball M d × P ball M d Bnd P ball M d
78 bndss M P ball M d × P ball M d Bnd P ball M d Y P ball M d M P ball M d × P ball M d Y × Y Bnd Y
79 77 69 78 syl2anc M Met X P X d Y P ball M d M P ball M d × P ball M d Y × Y Bnd Y
80 73 79 eqeltrrd M Met X P X d Y P ball M d N Bnd Y
81 80 rexlimdvaa M Met X P X d Y P ball M d N Bnd Y
82 68 81 impbid M Met X P X N Bnd Y d Y P ball M d