Definition df-ucn 23336

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 𝑓 is uniformly continuous if, roughly speaking, it is possible to guarantee that (𝑓‘𝑥) and (𝑓‘𝑦) be as close to each other as we please by requiring only that 𝑥 and 𝑦 are sufficiently close to each other; unlike ordinary continuity, the maximum distance between (𝑓‘𝑥) and (𝑓‘𝑦) cannot depend on 𝑥 and 𝑦 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 = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})

Distinct variable group:   𝑣,𝑢,𝑓,𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-ucn

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

This definition is referenced by:  ucnval  23337