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 ∈ ⋃ ran ⁡ UnifOn , v ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ dom ⁡ ⋃ v dom ⁡ ⋃ u | ∀ s ∈ v ∃ r ∈ u ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cucn class uCn
1 vu setvar u
2 cust class UnifOn
3 2 crn class ran ⁡ UnifOn
4 3 cuni class ⋃ ran ⁡ UnifOn
5 vv setvar v
6 vf setvar f
7 5 cv setvar v
8 7 cuni class ⋃ v
9 8 cdm class dom ⁡ ⋃ v
10 cmap class ↑ 𝑚
11 1 cv setvar u
12 11 cuni class ⋃ u
13 12 cdm class dom ⁡ ⋃ u
14 9 13 10 co class dom ⁡ ⋃ v dom ⁡ ⋃ u
15 vs setvar s
16 vr setvar r
17 vx setvar x
18 vy setvar y
19 17 cv setvar x
20 16 cv setvar r
21 18 cv setvar y
22 19 21 20 wbr wff x r y
23 6 cv setvar f
24 19 23 cfv class f ⁡ x
25 15 cv setvar s
26 21 23 cfv class f ⁡ y
27 24 26 25 wbr wff f ⁡ x s f ⁡ y
28 22 27 wi wff x r y → f ⁡ x s f ⁡ y
29 28 18 13 wral wff ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y
30 29 17 13 wral wff ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y
31 30 16 11 wrex wff ∃ r ∈ u ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y
32 31 15 7 wral wff ∀ s ∈ v ∃ r ∈ u ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y
33 32 6 14 crab class f ∈ dom ⁡ ⋃ v dom ⁡ ⋃ u | ∀ s ∈ v ∃ r ∈ u ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y
34 1 5 4 4 33 cmpo class u ∈ ⋃ ran ⁡ UnifOn , v ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ dom ⁡ ⋃ v dom ⁡ ⋃ u | ∀ s ∈ v ∃ r ∈ u ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y
35 0 34 wceq wff uCn = u ∈ ⋃ ran ⁡ UnifOn , v ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ dom ⁡ ⋃ v dom ⁡ ⋃ u | ∀ s ∈ v ∃ r ∈ u ∀ x ∈ dom ⁡ ⋃ u ∀ y ∈ dom ⁡ ⋃ u x r y → f ⁡ x s f ⁡ y