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 𝑋 ) ∣ ∀ 𝑠 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝑓 ‘ 𝑥 ) 𝑠 ( 𝑓 ‘ 𝑦 ) ) } )