Step |
Hyp |
Ref |
Expression |
1 |
|
blrnps |
|- ( D e. ( PsMet ` X ) -> ( B e. ran ( ball ` D ) <-> E. y e. X E. r e. RR* B = ( y ( ball ` D ) r ) ) ) |
2 |
|
elblps |
|- ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) -> ( P e. ( y ( ball ` D ) r ) <-> ( P e. X /\ ( y D P ) < r ) ) ) |
3 |
|
simpl1 |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> D e. ( PsMet ` X ) ) |
4 |
|
simpl2 |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> y e. X ) |
5 |
|
simpr |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> P e. X ) |
6 |
|
psmetcl |
|- ( ( D e. ( PsMet ` X ) /\ y e. X /\ P e. X ) -> ( y D P ) e. RR* ) |
7 |
3 4 5 6
|
syl3anc |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> ( y D P ) e. RR* ) |
8 |
|
simpl3 |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> r e. RR* ) |
9 |
|
qbtwnxr |
|- ( ( ( y D P ) e. RR* /\ r e. RR* /\ ( y D P ) < r ) -> E. z e. QQ ( ( y D P ) < z /\ z < r ) ) |
10 |
9
|
3expia |
|- ( ( ( y D P ) e. RR* /\ r e. RR* ) -> ( ( y D P ) < r -> E. z e. QQ ( ( y D P ) < z /\ z < r ) ) ) |
11 |
7 8 10
|
syl2anc |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> ( ( y D P ) < r -> E. z e. QQ ( ( y D P ) < z /\ z < r ) ) ) |
12 |
|
qre |
|- ( z e. QQ -> z e. RR ) |
13 |
|
simpll1 |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> D e. ( PsMet ` X ) ) |
14 |
|
simplr |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> P e. X ) |
15 |
|
simpll2 |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> y e. X ) |
16 |
|
psmetsym |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ y e. X ) -> ( P D y ) = ( y D P ) ) |
17 |
13 14 15 16
|
syl3anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) = ( y D P ) ) |
18 |
|
simprrl |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( y D P ) < z ) |
19 |
17 18
|
eqbrtrd |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) < z ) |
20 |
|
simprl |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> z e. RR ) |
21 |
|
psmetcl |
|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ y e. X ) -> ( P D y ) e. RR* ) |
22 |
13 14 15 21
|
syl3anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) e. RR* ) |
23 |
|
rexr |
|- ( z e. RR -> z e. RR* ) |
24 |
23
|
ad2antrl |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> z e. RR* ) |
25 |
22 24 19
|
xrltled |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) <_ z ) |
26 |
|
psmetlecl |
|- ( ( D e. ( PsMet ` X ) /\ ( P e. X /\ y e. X ) /\ ( z e. RR /\ ( P D y ) <_ z ) ) -> ( P D y ) e. RR ) |
27 |
13 14 15 20 25 26
|
syl122anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) e. RR ) |
28 |
|
difrp |
|- ( ( ( P D y ) e. RR /\ z e. RR ) -> ( ( P D y ) < z <-> ( z - ( P D y ) ) e. RR+ ) ) |
29 |
27 20 28
|
syl2anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( ( P D y ) < z <-> ( z - ( P D y ) ) e. RR+ ) ) |
30 |
19 29
|
mpbid |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( z - ( P D y ) ) e. RR+ ) |
31 |
20 27
|
resubcld |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( z - ( P D y ) ) e. RR ) |
32 |
22
|
xrleidd |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) <_ ( P D y ) ) |
33 |
20
|
recnd |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> z e. CC ) |
34 |
27
|
recnd |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) e. CC ) |
35 |
33 34
|
nncand |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( z - ( z - ( P D y ) ) ) = ( P D y ) ) |
36 |
32 35
|
breqtrrd |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P D y ) <_ ( z - ( z - ( P D y ) ) ) ) |
37 |
|
blss2ps |
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ y e. X ) /\ ( ( z - ( P D y ) ) e. RR /\ z e. RR /\ ( P D y ) <_ ( z - ( z - ( P D y ) ) ) ) ) -> ( P ( ball ` D ) ( z - ( P D y ) ) ) C_ ( y ( ball ` D ) z ) ) |
38 |
13 14 15 31 20 36 37
|
syl33anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P ( ball ` D ) ( z - ( P D y ) ) ) C_ ( y ( ball ` D ) z ) ) |
39 |
|
simpll3 |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> r e. RR* ) |
40 |
|
simprrr |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> z < r ) |
41 |
24 39 40
|
xrltled |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> z <_ r ) |
42 |
|
ssblps |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X ) /\ ( z e. RR* /\ r e. RR* ) /\ z <_ r ) -> ( y ( ball ` D ) z ) C_ ( y ( ball ` D ) r ) ) |
43 |
13 15 24 39 41 42
|
syl221anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( y ( ball ` D ) z ) C_ ( y ( ball ` D ) r ) ) |
44 |
38 43
|
sstrd |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> ( P ( ball ` D ) ( z - ( P D y ) ) ) C_ ( y ( ball ` D ) r ) ) |
45 |
|
oveq2 |
|- ( x = ( z - ( P D y ) ) -> ( P ( ball ` D ) x ) = ( P ( ball ` D ) ( z - ( P D y ) ) ) ) |
46 |
45
|
sseq1d |
|- ( x = ( z - ( P D y ) ) -> ( ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) <-> ( P ( ball ` D ) ( z - ( P D y ) ) ) C_ ( y ( ball ` D ) r ) ) ) |
47 |
46
|
rspcev |
|- ( ( ( z - ( P D y ) ) e. RR+ /\ ( P ( ball ` D ) ( z - ( P D y ) ) ) C_ ( y ( ball ` D ) r ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) |
48 |
30 44 47
|
syl2anc |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ ( z e. RR /\ ( ( y D P ) < z /\ z < r ) ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) |
49 |
48
|
expr |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ z e. RR ) -> ( ( ( y D P ) < z /\ z < r ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
50 |
12 49
|
sylan2 |
|- ( ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) /\ z e. QQ ) -> ( ( ( y D P ) < z /\ z < r ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
51 |
50
|
rexlimdva |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> ( E. z e. QQ ( ( y D P ) < z /\ z < r ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
52 |
11 51
|
syld |
|- ( ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) /\ P e. X ) -> ( ( y D P ) < r -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
53 |
52
|
expimpd |
|- ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) -> ( ( P e. X /\ ( y D P ) < r ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
54 |
2 53
|
sylbid |
|- ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) -> ( P e. ( y ( ball ` D ) r ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
55 |
|
eleq2 |
|- ( B = ( y ( ball ` D ) r ) -> ( P e. B <-> P e. ( y ( ball ` D ) r ) ) ) |
56 |
|
sseq2 |
|- ( B = ( y ( ball ` D ) r ) -> ( ( P ( ball ` D ) x ) C_ B <-> ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
57 |
56
|
rexbidv |
|- ( B = ( y ( ball ` D ) r ) -> ( E. x e. RR+ ( P ( ball ` D ) x ) C_ B <-> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) |
58 |
55 57
|
imbi12d |
|- ( B = ( y ( ball ` D ) r ) -> ( ( P e. B -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B ) <-> ( P e. ( y ( ball ` D ) r ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( y ( ball ` D ) r ) ) ) ) |
59 |
54 58
|
syl5ibrcom |
|- ( ( D e. ( PsMet ` X ) /\ y e. X /\ r e. RR* ) -> ( B = ( y ( ball ` D ) r ) -> ( P e. B -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B ) ) ) |
60 |
59
|
3expib |
|- ( D e. ( PsMet ` X ) -> ( ( y e. X /\ r e. RR* ) -> ( B = ( y ( ball ` D ) r ) -> ( P e. B -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B ) ) ) ) |
61 |
60
|
rexlimdvv |
|- ( D e. ( PsMet ` X ) -> ( E. y e. X E. r e. RR* B = ( y ( ball ` D ) r ) -> ( P e. B -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B ) ) ) |
62 |
1 61
|
sylbid |
|- ( D e. ( PsMet ` X ) -> ( B e. ran ( ball ` D ) -> ( P e. B -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B ) ) ) |
63 |
62
|
3imp |
|- ( ( D e. ( PsMet ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B ) |