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	⊢ Cnu = ( 𝑢 ∈ ∪ ran UnifOn , 𝑣 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) ∣ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cucn	⊢ Cnu
1		vu	⊢ 𝑢
2		cust	⊢ UnifOn
3	2	crn	⊢ ran UnifOn
4	3	cuni	⊢ ∪ ran UnifOn
5		vv	⊢ 𝑣
6		vf	⊢ 𝑓
7	5	cv	⊢ 𝑣
8	7	cuni	⊢ ∪ 𝑣
9	8	cdm	⊢ dom ∪ 𝑣
10		cmap	⊢ ↑m
11	1	cv	⊢ 𝑢
12	11	cuni	⊢ ∪ 𝑢
13	12	cdm	⊢ dom ∪ 𝑢
14	9 13 10	co	⊢ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 )
15		vs	⊢ 𝑠
16		vr	⊢ 𝑟
17		vx	⊢ 𝑥
18		vy	⊢ 𝑦
19	17	cv	⊢ 𝑥
20	16	cv	⊢ 𝑟
21	18	cv	⊢ 𝑦
22	19 21 20	wbr	⊢ 𝑥 𝑟 𝑦
23	6	cv	⊢ 𝑓
24	19 23	cfv	⊢ ( 𝑓 ‘ 𝑥 )
25	15	cv	⊢ 𝑠
26	21 23	cfv	⊢ ( 𝑓 ‘ 𝑦 )
27	24 26 25	wbr	⊢ ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 )
28	22 27	wi	⊢ ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) )
29	28 18 13	wral	⊢ ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) )
30	29 17 13	wral	⊢ ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) )
31	30 16 11	wrex	⊢ ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) )
32	31 15 7	wral	⊢ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) )
33	32 6 14	crab	⊢ { 𝑓 ∈ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) ∣ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) }
34	1 5 4 4 33	cmpo	⊢ ( 𝑢 ∈ ∪ ran UnifOn , 𝑣 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) ∣ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } )
35	0 34	wceq	⊢ Cnu = ( 𝑢 ∈ ∪ ran UnifOn , 𝑣 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( dom ∪ 𝑣 ↑m dom ∪ 𝑢 ) ∣ ∀ 𝑠 ∈ 𝑣 ∃ 𝑟 ∈ 𝑢 ∀ 𝑥 ∈ dom ∪ 𝑢 ∀ 𝑦 ∈ dom ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } )