Metamath Proof Explorer

Theorem metcnp3

Description: Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of Gleason p. 240. (Contributed by NM, 17-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses metcn.2 
|- J = ( MetOpen ` C )
metcn.4 
|- K = ( MetOpen ` D )
Assertion metcnp3 
|- ( ( 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 ) ) ) )

Proof

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