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 ) ) } )