Definition df-ucn 22080

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 ( f ` x ) and ( f ` y ) 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 ( f ` x ) and ( f ` y ) 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.)

Assertion

Ref	Expression
df-ucn	|- Cnu = ( 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 ) ) } )

Distinct variable group:   v, u, f, s, r, x, y

Detailed syntax breakdown of Definition df-ucn

Step	Hyp	Ref	Expression
1		cucn 22079	. 2 class Cnu
2		vu	. . 3 setvar u
3		vv	. . 3 setvar v
4		cust 22003	. . . . 5 class UnifOn
5	4	crn 5115	. . . 4 class ran UnifOn
6	5	cuni 4436	. . 3 class U. ran UnifOn
7		vx	. . . . . . . . . . 11 setvar x
8	7	cv 1482	. . . . . . . . . 10 class x
9		vy	. . . . . . . . . . 11 setvar y
10	9	cv 1482	. . . . . . . . . 10 class y
11		vr	. . . . . . . . . . 11 setvar r
12	11	cv 1482	. . . . . . . . . 10 class r
13	8, 10, 12	wbr 4653	. . . . . . . . 9 wff x r y
14		vf	. . . . . . . . . . . 12 setvar f
15	14	cv 1482	. . . . . . . . . . 11 class f
16	8, 15	cfv 5888	. . . . . . . . . 10 class ( f ` x )
17	10, 15	cfv 5888	. . . . . . . . . 10 class ( f ` y )
18		vs	. . . . . . . . . . 11 setvar s
19	18	cv 1482	. . . . . . . . . 10 class s
20	16, 17, 19	wbr 4653	. . . . . . . . 9 wff ( f ` x ) s ( f ` y )
21	13, 20	wi 4	. . . . . . . 8 wff ( x r y -> ( f ` x ) s ( f ` y ) )
22	2	cv 1482	. . . . . . . . . 10 class u
23	22	cuni 4436	. . . . . . . . 9 class U. u
24	23	cdm 5114	. . . . . . . 8 class dom U. u
25	21, 9, 24	wral 2912	. . . . . . 7 wff A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
26	25, 7, 24	wral 2912	. . . . . 6 wff A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
27	26, 11, 22	wrex 2913	. . . . 5 wff E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) )
28	3	cv 1482	. . . . 5 class v
29	27, 18, 28	wral 2912	. . . 4 wff 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 ) )
30	28	cuni 4436	. . . . . 6 class U. v
31	30	cdm 5114	. . . . 5 class dom U. v
32		cmap 7857	. . . . 5 class ^m
33	31, 24, 32	co 6650	. . . 4 class ( dom U. v ^m dom U. u )
34	29, 14, 33	crab 2916	. . 3 class { 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	2, 3, 6, 6, 34	cmpt2 6652	. 2 class ( 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 ) ) } )
36	1, 35	wceq 1483	1 wff Cnu = ( 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 ) ) } )

This definition is referenced by:  ucnval  22081