Metamath Proof Explorer

Theorem metucn

Description: Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn . (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypotheses metucn.u 
|- U = ( metUnif ` C )
metucn.v 
|- V = ( metUnif ` D )
metucn.x 
|- ( ph -> X =/= (/) )
metucn.y 
|- ( ph -> Y =/= (/) )
metucn.c 
|- ( ph -> C e. ( PsMet ` X ) )
metucn.d 
|- ( ph -> D e. ( PsMet ` Y ) )
Assertion metucn 
|- ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) ) )

Proof

Step Hyp Ref Expression
1 metucn.u 
 |-  U = ( metUnif ` C )
2 metucn.v 
 |-  V = ( metUnif ` D )
3 metucn.x 
 |-  ( ph -> X =/= (/) )
4 metucn.y 
 |-  ( ph -> Y =/= (/) )
5 metucn.c 
 |-  ( ph -> C e. ( PsMet ` X ) )
6 metucn.d 
 |-  ( ph -> D e. ( PsMet ` Y ) )
7 metuval 
 |-  ( C e. ( PsMet ` X ) -> ( metUnif ` C ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) )
8 5 7 syl 
 |-  ( ph -> ( metUnif ` C ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) )
9 1 8 syl5eq 
 |-  ( ph -> U = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) )
10 metuval 
 |-  ( D e. ( PsMet ` Y ) -> ( metUnif ` D ) = ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) )
11 6 10 syl 
 |-  ( ph -> ( metUnif ` D ) = ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) )
12 2 11 syl5eq 
 |-  ( ph -> V = ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) )
13 9 12 oveq12d 
 |-  ( ph -> ( U uCn V ) = ( ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) uCn ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) ) )
14 13 eleq2d 
 |-  ( ph -> ( F e. ( U uCn V ) <-> F e. ( ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) uCn ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) ) ) )
15 eqid 
 |-  ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) )
16 eqid 
 |-  ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) = ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) )
17 oveq2 
 |-  ( a = c -> ( 0 [,) a ) = ( 0 [,) c ) )
18 17 imaeq2d 
 |-  ( a = c -> ( `' C " ( 0 [,) a ) ) = ( `' C " ( 0 [,) c ) ) )
19 18 cbvmptv 
 |-  ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) = ( c e. RR+ |-> ( `' C " ( 0 [,) c ) ) )
20 19 rneqi 
 |-  ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) = ran ( c e. RR+ |-> ( `' C " ( 0 [,) c ) ) )
21 20 metust 
 |-  ( ( X =/= (/) /\ C e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) e. ( UnifOn ` X ) )
22 3 5 21 syl2anc 
 |-  ( ph -> ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) e. ( UnifOn ` X ) )
23 oveq2 
 |-  ( b = d -> ( 0 [,) b ) = ( 0 [,) d ) )
24 23 imaeq2d 
 |-  ( b = d -> ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) d ) ) )
25 24 cbvmptv 
 |-  ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) = ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) )
26 25 rneqi 
 |-  ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) = ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) )
27 26 metust 
 |-  ( ( Y =/= (/) /\ D e. ( PsMet ` Y ) ) -> ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) e. ( UnifOn ` Y ) )
28 4 6 27 syl2anc 
 |-  ( ph -> ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) e. ( UnifOn ` Y ) )
29 oveq2 
 |-  ( a = e -> ( 0 [,) a ) = ( 0 [,) e ) )
30 29 imaeq2d 
 |-  ( a = e -> ( `' C " ( 0 [,) a ) ) = ( `' C " ( 0 [,) e ) ) )
31 30 cbvmptv 
 |-  ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) = ( e e. RR+ |-> ( `' C " ( 0 [,) e ) ) )
32 31 rneqi 
 |-  ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) = ran ( e e. RR+ |-> ( `' C " ( 0 [,) e ) ) )
33 32 metustfbas 
 |-  ( ( X =/= (/) /\ C e. ( PsMet ` X ) ) -> ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) e. ( fBas ` ( X X. X ) ) )
34 3 5 33 syl2anc 
 |-  ( ph -> ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) e. ( fBas ` ( X X. X ) ) )
35 oveq2 
 |-  ( b = f -> ( 0 [,) b ) = ( 0 [,) f ) )
36 35 imaeq2d 
 |-  ( b = f -> ( `' D " ( 0 [,) b ) ) = ( `' D " ( 0 [,) f ) ) )
37 36 cbvmptv 
 |-  ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) = ( f e. RR+ |-> ( `' D " ( 0 [,) f ) ) )
38 37 rneqi 
 |-  ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) = ran ( f e. RR+ |-> ( `' D " ( 0 [,) f ) ) )
39 38 metustfbas 
 |-  ( ( Y =/= (/) /\ D e. ( PsMet ` Y ) ) -> ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) e. ( fBas ` ( Y X. Y ) ) )
40 4 6 39 syl2anc 
 |-  ( ph -> ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) e. ( fBas ` ( Y X. Y ) ) )
41 15 16 22 28 34 40 isucn2 
 |-  ( ph -> ( F e. ( ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) ) uCn ( ( Y X. Y ) filGen ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) ) ) <-> ( F : X --> Y /\ A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) ) )
42 14 41 bitrd 
 |-  ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) ) )
43 eqid 
 |-  ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) d ) )
44 oveq2 
 |-  ( f = d -> ( 0 [,) f ) = ( 0 [,) d ) )
45 44 imaeq2d 
 |-  ( f = d -> ( `' D " ( 0 [,) f ) ) = ( `' D " ( 0 [,) d ) ) )
46 45 rspceeqv 
 |-  ( ( d e. RR+ /\ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) d ) ) ) -> E. f e. RR+ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) f ) ) )
47 43 46 mpan2 
 |-  ( d e. RR+ -> E. f e. RR+ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) f ) ) )
48 47 adantl 
 |-  ( ( ph /\ d e. RR+ ) -> E. f e. RR+ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) f ) ) )
49 38 metustel 
 |-  ( D e. ( PsMet ` Y ) -> ( ( `' D " ( 0 [,) d ) ) e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) <-> E. f e. RR+ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) f ) ) ) )
50 6 49 syl 
 |-  ( ph -> ( ( `' D " ( 0 [,) d ) ) e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) <-> E. f e. RR+ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) f ) ) ) )
51 50 adantr 
 |-  ( ( ph /\ d e. RR+ ) -> ( ( `' D " ( 0 [,) d ) ) e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) <-> E. f e. RR+ ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) f ) ) ) )
52 48 51 mpbird 
 |-  ( ( ph /\ d e. RR+ ) -> ( `' D " ( 0 [,) d ) ) e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) )
53 26 metustel 
 |-  ( D e. ( PsMet ` Y ) -> ( v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) <-> E. d e. RR+ v = ( `' D " ( 0 [,) d ) ) ) )
54 6 53 syl 
 |-  ( ph -> ( v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) <-> E. d e. RR+ v = ( `' D " ( 0 [,) d ) ) ) )
55 simpr 
 |-  ( ( ph /\ v = ( `' D " ( 0 [,) d ) ) ) -> v = ( `' D " ( 0 [,) d ) ) )
56 55 breqd 
 |-  ( ( ph /\ v = ( `' D " ( 0 [,) d ) ) ) -> ( ( F ` x ) v ( F ` y ) <-> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) )
57 56 imbi2d 
 |-  ( ( ph /\ v = ( `' D " ( 0 [,) d ) ) ) -> ( ( x u y -> ( F ` x ) v ( F ` y ) ) <-> ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
58 57 ralbidv 
 |-  ( ( ph /\ v = ( `' D " ( 0 [,) d ) ) ) -> ( A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. y e. X ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
59 58 rexralbidv 
 |-  ( ( ph /\ v = ( `' D " ( 0 [,) d ) ) ) -> ( E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
60 52 54 59 ralxfr2d 
 |-  ( ph -> ( A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. d e. RR+ E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
61 eqid 
 |-  ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) c ) )
62 oveq2 
 |-  ( e = c -> ( 0 [,) e ) = ( 0 [,) c ) )
63 62 imaeq2d 
 |-  ( e = c -> ( `' C " ( 0 [,) e ) ) = ( `' C " ( 0 [,) c ) ) )
64 63 rspceeqv 
 |-  ( ( c e. RR+ /\ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) c ) ) ) -> E. e e. RR+ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) e ) ) )
65 61 64 mpan2 
 |-  ( c e. RR+ -> E. e e. RR+ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) e ) ) )
66 65 adantl 
 |-  ( ( ph /\ c e. RR+ ) -> E. e e. RR+ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) e ) ) )
67 32 metustel 
 |-  ( C e. ( PsMet ` X ) -> ( ( `' C " ( 0 [,) c ) ) e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) <-> E. e e. RR+ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) e ) ) ) )
68 5 67 syl 
 |-  ( ph -> ( ( `' C " ( 0 [,) c ) ) e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) <-> E. e e. RR+ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) e ) ) ) )
69 68 adantr 
 |-  ( ( ph /\ c e. RR+ ) -> ( ( `' C " ( 0 [,) c ) ) e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) <-> E. e e. RR+ ( `' C " ( 0 [,) c ) ) = ( `' C " ( 0 [,) e ) ) ) )
70 66 69 mpbird 
 |-  ( ( ph /\ c e. RR+ ) -> ( `' C " ( 0 [,) c ) ) e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) )
71 20 metustel 
 |-  ( C e. ( PsMet ` X ) -> ( u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) <-> E. c e. RR+ u = ( `' C " ( 0 [,) c ) ) ) )
72 5 71 syl 
 |-  ( ph -> ( u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) <-> E. c e. RR+ u = ( `' C " ( 0 [,) c ) ) ) )
73 simpr 
 |-  ( ( ph /\ u = ( `' C " ( 0 [,) c ) ) ) -> u = ( `' C " ( 0 [,) c ) ) )
74 73 breqd 
 |-  ( ( ph /\ u = ( `' C " ( 0 [,) c ) ) ) -> ( x u y <-> x ( `' C " ( 0 [,) c ) ) y ) )
75 74 imbi1d 
 |-  ( ( ph /\ u = ( `' C " ( 0 [,) c ) ) ) -> ( ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
76 75 2ralbidv 
 |-  ( ( ph /\ u = ( `' C " ( 0 [,) c ) ) ) -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
77 70 72 76 rexxfr2d 
 |-  ( ph -> ( E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> E. c e. RR+ A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
78 77 ralbidv 
 |-  ( ph -> ( A. d e. RR+ E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
79 60 78 bitrd 
 |-  ( ph -> ( A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
80 79 adantr 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) ) )
81 5 ad4antr 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> C e. ( PsMet ` X ) )
82 simplr 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> c e. RR+ )
83 simprr 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> y e. X )
84 simprl 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> x e. X )
85 elbl4 
 |-  ( ( ( C e. ( PsMet ` X ) /\ c e. RR+ ) /\ ( y e. X /\ x e. X ) ) -> ( x e. ( y ( ball ` C ) c ) <-> x ( `' C " ( 0 [,) c ) ) y ) )
86 rpxr 
 |-  ( c e. RR+ -> c e. RR* )
87 elbl3ps 
 |-  ( ( ( C e. ( PsMet ` X ) /\ c e. RR* ) /\ ( y e. X /\ x e. X ) ) -> ( x e. ( y ( ball ` C ) c ) <-> ( x C y ) < c ) )
88 86 87 sylanl2 
 |-  ( ( ( C e. ( PsMet ` X ) /\ c e. RR+ ) /\ ( y e. X /\ x e. X ) ) -> ( x e. ( y ( ball ` C ) c ) <-> ( x C y ) < c ) )
89 85 88 bitr3d 
 |-  ( ( ( C e. ( PsMet ` X ) /\ c e. RR+ ) /\ ( y e. X /\ x e. X ) ) -> ( x ( `' C " ( 0 [,) c ) ) y <-> ( x C y ) < c ) )
90 81 82 83 84 89 syl22anc 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( x ( `' C " ( 0 [,) c ) ) y <-> ( x C y ) < c ) )
91 6 ad4antr 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> D e. ( PsMet ` Y ) )
92 simpllr 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> d e. RR+ )
93 simp-4r 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> F : X --> Y )
94 93 83 ffvelrnd 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( F ` y ) e. Y )
95 93 84 ffvelrnd 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( F ` x ) e. Y )
96 elbl4 
 |-  ( ( ( D e. ( PsMet ` Y ) /\ d e. RR+ ) /\ ( ( F ` y ) e. Y /\ ( F ` x ) e. Y ) ) -> ( ( F ` x ) e. ( ( F ` y ) ( ball ` D ) d ) <-> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) )
97 rpxr 
 |-  ( d e. RR+ -> d e. RR* )
98 elbl3ps 
 |-  ( ( ( D e. ( PsMet ` Y ) /\ d e. RR* ) /\ ( ( F ` y ) e. Y /\ ( F ` x ) e. Y ) ) -> ( ( F ` x ) e. ( ( F ` y ) ( ball ` D ) d ) <-> ( ( F ` x ) D ( F ` y ) ) < d ) )
99 97 98 sylanl2 
 |-  ( ( ( D e. ( PsMet ` Y ) /\ d e. RR+ ) /\ ( ( F ` y ) e. Y /\ ( F ` x ) e. Y ) ) -> ( ( F ` x ) e. ( ( F ` y ) ( ball ` D ) d ) <-> ( ( F ` x ) D ( F ` y ) ) < d ) )
100 96 99 bitr3d 
 |-  ( ( ( D e. ( PsMet ` Y ) /\ d e. RR+ ) /\ ( ( F ` y ) e. Y /\ ( F ` x ) e. Y ) ) -> ( ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) <-> ( ( F ` x ) D ( F ` y ) ) < d ) )
101 91 92 94 95 100 syl22anc 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) <-> ( ( F ` x ) D ( F ` y ) ) < d ) )
102 90 101 imbi12d 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) )
103 102 2ralbidva 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) /\ c e. RR+ ) -> ( A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) )
104 103 rexbidva 
 |-  ( ( ( ph /\ F : X --> Y ) /\ d e. RR+ ) -> ( E. c e. RR+ A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) )
105 104 ralbidva 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( x ( `' C " ( 0 [,) c ) ) y -> ( F ` x ) ( `' D " ( 0 [,) d ) ) ( F ` y ) ) <-> A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) )
106 80 105 bitrd 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) )
107 106 pm5.32da 
 |-  ( ph -> ( ( F : X --> Y /\ A. v e. ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) ) E. u e. ran ( a e. RR+ |-> ( `' C " ( 0 [,) a ) ) ) A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) <-> ( F : X --> Y /\ A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) ) )
108 42 107 bitrd 
 |-  ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) ) )