This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ucn

Description: Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function f is uniformly continuous if, roughly speaking, it is possible to guarantee that ( fx ) and ( fy ) be as close to each other as we please by requiring only that x and y are sufficiently close to each other; unlike ordinary continuity, the maximum distance between ( fx ) and ( fy ) cannot depend on x and y themselves. This formulation is the definition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion df-ucn 
|- uCn = ( u e. U. ran UnifOn , v e. U. ran UnifOn |-> { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cucn 
 |-  uCn
1 vu 
 |-  u
2 cust 
 |-  UnifOn
3 2 crn 
 |-  ran UnifOn
4 3 cuni 
 |-  U. ran UnifOn
5 vv 
 |-  v
6 vf 
 |-  f
7 5 cv 
 |-  v
8 7 cuni 
 |-  U. v
9 8 cdm 
 |-  dom U. v
10 cmap 
 |-  ^m
11 1 cv 
 |-  u
12 11 cuni 
 |-  U. u
13 12 cdm 
 |-  dom U. u
14 9 13 10 co 
 |-  ( dom U. v ^m dom U. u )
15 vs 
 |-  s
16 vr 
 |-  r
17 vx 
 |-  x
18 vy 
 |-  y
19 17 cv 
 |-  x
20 16 cv 
 |-  r
21 18 cv 
 |-  y
22 19 21 20 wbr 
 |-  x r y
23 6 cv 
 |-  f
24 19 23 cfv 
 |-  ( f ` x )
25 15 cv 
 |-  s
26 21 23 cfv 
 |-  ( f ` y )
27 24 26 25 wbr 
 |-  ( f ` x ) s ( f ` y )
28 22 27 wi 
 |-  ( x r y -> ( f ` x ) s ( f ` y ) )
29 28 18 13 wral 
 |-  A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
30 29 17 13 wral 
 |-  A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
31 30 16 11 wrex 
 |-  E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
32 31 15 7 wral 
 |-  A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
33 32 6 14 crab 
 |-  { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) }
34 1 5 4 4 33 cmpo 
 |-  ( u e. U. ran UnifOn , v e. U. ran UnifOn |-> { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) } )
35 0 34 wceq 
 |-  uCn = ( u e. U. ran UnifOn , v e. U. ran UnifOn |-> { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) } )