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 ) ) )