Metamath Proof Explorer


Theorem ucnval

Description: The set of all uniformly continuous function from uniform space U to uniform space V . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion ucnval ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( 𝑌m 𝑋 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥𝑋𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 elrnust ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ran UnifOn )
2 1 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → 𝑈 ran UnifOn )
3 elrnust ( 𝑉 ∈ ( UnifOn ‘ 𝑌 ) → 𝑉 ran UnifOn )
4 3 adantl ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → 𝑉 ran UnifOn )
5 ovex ( dom 𝑉m dom 𝑈 ) ∈ V
6 5 rabex { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } ∈ V
7 6 a1i ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } ∈ V )
8 simpr ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → 𝑣 = 𝑉 )
9 8 unieqd ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → 𝑣 = 𝑉 )
10 9 dmeqd ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → dom 𝑣 = dom 𝑉 )
11 simpl ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → 𝑢 = 𝑈 )
12 11 unieqd ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → 𝑢 = 𝑈 )
13 12 dmeqd ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → dom 𝑢 = dom 𝑈 )
14 10 13 oveq12d ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → ( dom 𝑣m dom 𝑢 ) = ( dom 𝑉m dom 𝑈 ) )
15 13 raleqdv ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → ( ∀ 𝑦 ∈ dom 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∀ 𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
16 13 15 raleqbidv ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → ( ∀ 𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
17 11 16 rexeqbidv ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → ( ∃ 𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∃ 𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
18 8 17 raleqbidv ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → ( ∀ 𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
19 14 18 rabeqbidv ( ( 𝑢 = 𝑈𝑣 = 𝑉 ) → { 𝑓 ∈ ( dom 𝑣m dom 𝑢 ) ∣ ∀ 𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } = { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )
20 df-ucn Cnu = ( 𝑢 ran UnifOn , 𝑣 ran UnifOn ↦ { 𝑓 ∈ ( dom 𝑣m dom 𝑢 ) ∣ ∀ 𝑠𝑣𝑟𝑢𝑥 ∈ dom 𝑢𝑦 ∈ dom 𝑢 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )
21 19 20 ovmpoga ( ( 𝑈 ran UnifOn ∧ 𝑉 ran UnifOn ∧ { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } ∈ V ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )
22 2 4 7 21 syl3anc ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )
23 ustbas2 ( 𝑉 ∈ ( UnifOn ‘ 𝑌 ) → 𝑌 = dom 𝑉 )
24 ustbas2 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom 𝑈 )
25 23 24 oveqan12rd ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑌m 𝑋 ) = ( dom 𝑉m dom 𝑈 ) )
26 24 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → 𝑋 = dom 𝑈 )
27 26 raleqdv ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∀ 𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∀ 𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
28 26 27 raleqbidv ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∀ 𝑥𝑋𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
29 28 rexbidv ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∃ 𝑟𝑈𝑥𝑋𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∃ 𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
30 29 ralbidv ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( ∀ 𝑠𝑉𝑟𝑈𝑥𝑋𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ↔ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) ) )
31 25 30 rabeqbidv ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → { 𝑓 ∈ ( 𝑌m 𝑋 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥𝑋𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } = { 𝑓 ∈ ( dom 𝑉m dom 𝑈 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥 ∈ dom 𝑈𝑦 ∈ dom 𝑈 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )
32 22 31 eqtr4d ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝑈 Cnu 𝑉 ) = { 𝑓 ∈ ( 𝑌m 𝑋 ) ∣ ∀ 𝑠𝑉𝑟𝑈𝑥𝑋𝑦𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓𝑥 ) 𝑠 ( 𝑓𝑦 ) ) } )