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

Metamath Proof Explorer

Theorem isucn

Description: The predicate " F is a uniformly continuous function from uniform space U to uniform space V ". (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion isucn 
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) } )
2 1 eleq2d 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> F e. { 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 ) ) } ) )
3 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
4 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
5 3 4 breq12d 
 |-  ( f = F -> ( ( f ` x ) s ( f ` y ) <-> ( F ` x ) s ( F ` y ) ) )
6 5 imbi2d 
 |-  ( f = F -> ( ( x r y -> ( f ` x ) s ( f ` y ) ) <-> ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
7 6 ralbidv 
 |-  ( f = F -> ( A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
8 7 rexralbidv 
 |-  ( f = F -> ( 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. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
9 8 ralbidv 
 |-  ( f = F -> ( 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. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
10 9 elrab 
 |-  ( F e. { 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. ( 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 ) ) ) )
11 2 10 bitrdi 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( 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 ) ) ) ) )
12 elfvex 
 |-  ( V e. ( UnifOn ` Y ) -> Y e. _V )
13 elfvex 
 |-  ( U e. ( UnifOn ` X ) -> X e. _V )
14 elmapg 
 |-  ( ( Y e. _V /\ X e. _V ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
15 12 13 14 syl2anr 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
16 15 anbi1d 
 |-  ( ( 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 : X --> 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 ) ) ) ) )
17 11 16 bitrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> 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 ) ) ) ) )