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