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
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( U uCn V ) = { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } )

Proof

Step Hyp Ref Expression
1 elrnust
 |-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )
2 1 adantr
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> U e. U. ran UnifOn )
3 elrnust
 |-  ( V e. ( UnifOn ` Y ) -> V e. U. ran UnifOn )
4 3 adantl
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> V e. U. ran UnifOn )
5 ovex
 |-  ( dom U. V ^m dom U. U ) e. _V
6 5 rabex
 |-  { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } e. _V
7 6 a1i
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } e. _V )
8 simpr
 |-  ( ( u = U /\ v = V ) -> v = V )
9 8 unieqd
 |-  ( ( u = U /\ v = V ) -> U. v = U. V )
10 9 dmeqd
 |-  ( ( u = U /\ v = V ) -> dom U. v = dom U. V )
11 simpl
 |-  ( ( u = U /\ v = V ) -> u = U )
12 11 unieqd
 |-  ( ( u = U /\ v = V ) -> U. u = U. U )
13 12 dmeqd
 |-  ( ( u = U /\ v = V ) -> dom U. u = dom U. U )
14 10 13 oveq12d
 |-  ( ( u = U /\ v = V ) -> ( dom U. v ^m dom U. u ) = ( dom U. V ^m dom U. U ) )
15 13 raleqdv
 |-  ( ( u = U /\ v = V ) -> ( A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
16 13 15 raleqbidv
 |-  ( ( u = U /\ v = V ) -> ( A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
17 11 16 rexeqbidv
 |-  ( ( u = U /\ v = V ) -> ( E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) <-> E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
18 8 17 raleqbidv
 |-  ( ( u = U /\ v = V ) -> ( A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
19 14 18 rabeqbidv
 |-  ( ( u = U /\ v = V ) -> { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) } = { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } )
20 df-ucn
 |-  uCn = ( u e. U. ran UnifOn , v e. U. ran UnifOn |-> { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) } )
21 19 20 ovmpoga
 |-  ( ( U e. U. ran UnifOn /\ V e. U. ran UnifOn /\ { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } e. _V ) -> ( U uCn V ) = { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } )
22 2 4 7 21 syl3anc
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( U uCn V ) = { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } )
23 ustbas2
 |-  ( V e. ( UnifOn ` Y ) -> Y = dom U. V )
24 ustbas2
 |-  ( U e. ( UnifOn ` X ) -> X = dom U. U )
25 23 24 oveqan12rd
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( Y ^m X ) = ( dom U. V ^m dom U. U ) )
26 24 adantr
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> X = dom U. U )
27 26 raleqdv
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
28 26 27 raleqbidv
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
29 28 rexbidv
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
30 29 ralbidv
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) ) )
31 25 30 rabeqbidv
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } = { f e. ( dom U. V ^m dom U. U ) | A. s e. V E. r e. U A. x e. dom U. U A. y e. dom U. U ( x r y -> ( f ` x ) s ( f ` y ) ) } )
32 22 31 eqtr4d
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( U uCn V ) = { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } )