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 X. Y ) )
Assertion ssbnd
|- ( ( M e. ( Met ` X ) /\ P e. X ) -> ( N e. ( Bnd ` Y ) <-> E. d e. RR Y C_ ( P ( ball ` M ) d ) ) )

Proof

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