Step |
Hyp |
Ref |
Expression |
1 |
|
metcn.2 |
|- J = ( MetOpen ` C ) |
2 |
|
metcn.4 |
|- K = ( MetOpen ` D ) |
3 |
1
|
mopntopon |
|- ( C e. ( *Met ` X ) -> J e. ( TopOn ` X ) ) |
4 |
3
|
3ad2ant1 |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> J e. ( TopOn ` X ) ) |
5 |
2
|
mopnval |
|- ( D e. ( *Met ` Y ) -> K = ( topGen ` ran ( ball ` D ) ) ) |
6 |
5
|
3ad2ant2 |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> K = ( topGen ` ran ( ball ` D ) ) ) |
7 |
2
|
mopntopon |
|- ( D e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) ) |
8 |
7
|
3ad2ant2 |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> K e. ( TopOn ` Y ) ) |
9 |
|
simp3 |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> P e. X ) |
10 |
4 6 8 9
|
tgcnp |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) ) |
11 |
|
simpll2 |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> D e. ( *Met ` Y ) ) |
12 |
|
simplr |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> F : X --> Y ) |
13 |
|
simpll3 |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> P e. X ) |
14 |
12 13
|
ffvelrnd |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( F ` P ) e. Y ) |
15 |
|
simpr |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> y e. RR+ ) |
16 |
|
blcntr |
|- ( ( D e. ( *Met ` Y ) /\ ( F ` P ) e. Y /\ y e. RR+ ) -> ( F ` P ) e. ( ( F ` P ) ( ball ` D ) y ) ) |
17 |
11 14 15 16
|
syl3anc |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( F ` P ) e. ( ( F ` P ) ( ball ` D ) y ) ) |
18 |
|
rpxr |
|- ( y e. RR+ -> y e. RR* ) |
19 |
18
|
adantl |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> y e. RR* ) |
20 |
|
blelrn |
|- ( ( D e. ( *Met ` Y ) /\ ( F ` P ) e. Y /\ y e. RR* ) -> ( ( F ` P ) ( ball ` D ) y ) e. ran ( ball ` D ) ) |
21 |
11 14 19 20
|
syl3anc |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( ( F ` P ) ( ball ` D ) y ) e. ran ( ball ` D ) ) |
22 |
|
eleq2 |
|- ( u = ( ( F ` P ) ( ball ` D ) y ) -> ( ( F ` P ) e. u <-> ( F ` P ) e. ( ( F ` P ) ( ball ` D ) y ) ) ) |
23 |
|
sseq2 |
|- ( u = ( ( F ` P ) ( ball ` D ) y ) -> ( ( F " v ) C_ u <-> ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
24 |
23
|
anbi2d |
|- ( u = ( ( F ` P ) ( ball ` D ) y ) -> ( ( P e. v /\ ( F " v ) C_ u ) <-> ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) |
25 |
24
|
rexbidv |
|- ( u = ( ( F ` P ) ( ball ` D ) y ) -> ( E. v e. J ( P e. v /\ ( F " v ) C_ u ) <-> E. v e. J ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) |
26 |
22 25
|
imbi12d |
|- ( u = ( ( F ` P ) ( ball ` D ) y ) -> ( ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) <-> ( ( F ` P ) e. ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) ) |
27 |
26
|
rspcv |
|- ( ( ( F ` P ) ( ball ` D ) y ) e. ran ( ball ` D ) -> ( A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) -> ( ( F ` P ) e. ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) ) |
28 |
21 27
|
syl |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) -> ( ( F ` P ) e. ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) ) |
29 |
17 28
|
mpid |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) |
30 |
|
simpl1 |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> C e. ( *Met ` X ) ) |
31 |
30
|
ad2antrr |
|- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ v e. J ) ) /\ P e. v ) -> C e. ( *Met ` X ) ) |
32 |
|
simplrr |
|- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ v e. J ) ) /\ P e. v ) -> v e. J ) |
33 |
|
simpr |
|- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ v e. J ) ) /\ P e. v ) -> P e. v ) |
34 |
1
|
mopni2 |
|- ( ( C e. ( *Met ` X ) /\ v e. J /\ P e. v ) -> E. z e. RR+ ( P ( ball ` C ) z ) C_ v ) |
35 |
31 32 33 34
|
syl3anc |
|- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ v e. J ) ) /\ P e. v ) -> E. z e. RR+ ( P ( ball ` C ) z ) C_ v ) |
36 |
|
sstr2 |
|- ( ( F " ( P ( ball ` C ) z ) ) C_ ( F " v ) -> ( ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) -> ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
37 |
|
imass2 |
|- ( ( P ( ball ` C ) z ) C_ v -> ( F " ( P ( ball ` C ) z ) ) C_ ( F " v ) ) |
38 |
36 37
|
syl11 |
|- ( ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) -> ( ( P ( ball ` C ) z ) C_ v -> ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
39 |
38
|
reximdv |
|- ( ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) -> ( E. z e. RR+ ( P ( ball ` C ) z ) C_ v -> E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
40 |
35 39
|
syl5com |
|- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ v e. J ) ) /\ P e. v ) -> ( ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) -> E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
41 |
40
|
expimpd |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ v e. J ) ) -> ( ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
42 |
41
|
expr |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( v e. J -> ( ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) |
43 |
42
|
rexlimdv |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( E. v e. J ( P e. v /\ ( F " v ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
44 |
29 43
|
syld |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) -> E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
45 |
44
|
ralrimdva |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) -> A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
46 |
|
simpl2 |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> D e. ( *Met ` Y ) ) |
47 |
|
blss |
|- ( ( D e. ( *Met ` Y ) /\ u e. ran ( ball ` D ) /\ ( F ` P ) e. u ) -> E. y e. RR+ ( ( F ` P ) ( ball ` D ) y ) C_ u ) |
48 |
47
|
3expib |
|- ( D e. ( *Met ` Y ) -> ( ( u e. ran ( ball ` D ) /\ ( F ` P ) e. u ) -> E. y e. RR+ ( ( F ` P ) ( ball ` D ) y ) C_ u ) ) |
49 |
46 48
|
syl |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( ( u e. ran ( ball ` D ) /\ ( F ` P ) e. u ) -> E. y e. RR+ ( ( F ` P ) ( ball ` D ) y ) C_ u ) ) |
50 |
|
r19.29r |
|- ( ( E. y e. RR+ ( ( F ` P ) ( ball ` D ) y ) C_ u /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. y e. RR+ ( ( ( F ` P ) ( ball ` D ) y ) C_ u /\ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
51 |
30
|
ad5ant12 |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> C e. ( *Met ` X ) ) |
52 |
13
|
ad2antrr |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> P e. X ) |
53 |
|
rpxr |
|- ( z e. RR+ -> z e. RR* ) |
54 |
53
|
ad2antrl |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> z e. RR* ) |
55 |
1
|
blopn |
|- ( ( C e. ( *Met ` X ) /\ P e. X /\ z e. RR* ) -> ( P ( ball ` C ) z ) e. J ) |
56 |
51 52 54 55
|
syl3anc |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> ( P ( ball ` C ) z ) e. J ) |
57 |
|
simprl |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> z e. RR+ ) |
58 |
|
blcntr |
|- ( ( C e. ( *Met ` X ) /\ P e. X /\ z e. RR+ ) -> P e. ( P ( ball ` C ) z ) ) |
59 |
51 52 57 58
|
syl3anc |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> P e. ( P ( ball ` C ) z ) ) |
60 |
|
sstr |
|- ( ( ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) -> ( F " ( P ( ball ` C ) z ) ) C_ u ) |
61 |
60
|
ad2ant2l |
|- ( ( ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) /\ ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) ) -> ( F " ( P ( ball ` C ) z ) ) C_ u ) |
62 |
61
|
ancoms |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> ( F " ( P ( ball ` C ) z ) ) C_ u ) |
63 |
|
eleq2 |
|- ( v = ( P ( ball ` C ) z ) -> ( P e. v <-> P e. ( P ( ball ` C ) z ) ) ) |
64 |
|
imaeq2 |
|- ( v = ( P ( ball ` C ) z ) -> ( F " v ) = ( F " ( P ( ball ` C ) z ) ) ) |
65 |
64
|
sseq1d |
|- ( v = ( P ( ball ` C ) z ) -> ( ( F " v ) C_ u <-> ( F " ( P ( ball ` C ) z ) ) C_ u ) ) |
66 |
63 65
|
anbi12d |
|- ( v = ( P ( ball ` C ) z ) -> ( ( P e. v /\ ( F " v ) C_ u ) <-> ( P e. ( P ( ball ` C ) z ) /\ ( F " ( P ( ball ` C ) z ) ) C_ u ) ) ) |
67 |
66
|
rspcev |
|- ( ( ( P ( ball ` C ) z ) e. J /\ ( P e. ( P ( ball ` C ) z ) /\ ( F " ( P ( ball ` C ) z ) ) C_ u ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) |
68 |
56 59 62 67
|
syl12anc |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ ( z e. RR+ /\ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) |
69 |
68
|
expr |
|- ( ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) /\ z e. RR+ ) -> ( ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) |
70 |
69
|
rexlimdva |
|- ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ ( ( F ` P ) ( ball ` D ) y ) C_ u ) -> ( E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) |
71 |
70
|
expimpd |
|- ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( ( ( ( F ` P ) ( ball ` D ) y ) C_ u /\ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) |
72 |
71
|
rexlimdva |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( E. y e. RR+ ( ( ( F ` P ) ( ball ` D ) y ) C_ u /\ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) |
73 |
50 72
|
syl5 |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( ( E. y e. RR+ ( ( F ` P ) ( ball ` D ) y ) C_ u /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) |
74 |
73
|
expd |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( E. y e. RR+ ( ( F ` P ) ( ball ` D ) y ) C_ u -> ( A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) |
75 |
49 74
|
syld |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( ( u e. ran ( ball ` D ) /\ ( F ` P ) e. u ) -> ( A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) |
76 |
75
|
com23 |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> ( ( u e. ran ( ball ` D ) /\ ( F ` P ) e. u ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) |
77 |
76
|
exp4a |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> ( u e. ran ( ball ` D ) -> ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) ) |
78 |
77
|
ralrimdv |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) -> A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) |
79 |
45 78
|
impbid |
|- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) <-> A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) |
80 |
79
|
pm5.32da |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( ( F : X --> Y /\ A. u e. ran ( ball ` D ) ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) |
81 |
10 80
|
bitrd |
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) ) |