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