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