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