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⁡⋃vdom⁡⋃u|∀s∈v∃r∈u∀x∈dom⁡⋃u∀y∈dom⁡⋃uxry→f⁡xsf⁡y

Detailed syntax breakdown

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