This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ∪ 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } )