Metamath Proof Explorer

Theorem ucnima

Description: An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Hypotheses ucnprima.1 
|- ( ph -> U e. ( UnifOn ` X ) )
ucnprima.2 
|- ( ph -> V e. ( UnifOn ` Y ) )
ucnprima.3 
|- ( ph -> F e. ( U uCn V ) )
ucnprima.4 
|- ( ph -> W e. V )
ucnprima.5 
|- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
Assertion ucnima 
|- ( ph -> E. r e. U ( G " r ) C_ W )

Proof

Step Hyp Ref Expression
1 ucnprima.1 
 |-  ( ph -> U e. ( UnifOn ` X ) )
2 ucnprima.2 
 |-  ( ph -> V e. ( UnifOn ` Y ) )
3 ucnprima.3 
 |-  ( ph -> F e. ( U uCn V ) )
4 ucnprima.4 
 |-  ( ph -> W e. V )
5 ucnprima.5 
 |-  G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
6 breq 
 |-  ( w = W -> ( ( F ` x ) w ( F ` y ) <-> ( F ` x ) W ( F ` y ) ) )
7 6 imbi2d 
 |-  ( w = W -> ( ( x r y -> ( F ` x ) w ( F ` y ) ) <-> ( x r y -> ( F ` x ) W ( F ` y ) ) ) )
8 7 ralbidv 
 |-  ( w = W -> ( A. y e. X ( x r y -> ( F ` x ) w ( F ` y ) ) <-> A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) )
9 8 rexralbidv 
 |-  ( w = W -> ( E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) w ( F ` y ) ) <-> E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) )
10 isucn 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. w e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) w ( F ` y ) ) ) ) )
11 1 2 10 syl2anc 
 |-  ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. w e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) w ( F ` y ) ) ) ) )
12 3 11 mpbid 
 |-  ( ph -> ( F : X --> Y /\ A. w e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) w ( F ` y ) ) ) )
13 12 simprd 
 |-  ( ph -> A. w e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) w ( F ` y ) ) )
14 9 13 4 rspcdva 
 |-  ( ph -> E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) )
15 simplll 
 |-  ( ( ( ( ph /\ r e. U ) /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. r ) -> ph )
16 simplr 
 |-  ( ( ( ( ph /\ r e. U ) /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. r ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) )
17 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ r e. U ) -> r C_ ( X X. X ) )
18 1 17 sylan 
 |-  ( ( ph /\ r e. U ) -> r C_ ( X X. X ) )
19 18 sselda 
 |-  ( ( ( ph /\ r e. U ) /\ p e. r ) -> p e. ( X X. X ) )
20 19 adantlr 
 |-  ( ( ( ( ph /\ r e. U ) /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. r ) -> p e. ( X X. X ) )
21 simpr 
 |-  ( ( ( ( ph /\ r e. U ) /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. r ) -> p e. r )
22 simplr 
 |-  ( ( ( ph /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. ( X X. X ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) )
23 elxp2 
 |-  ( p e. ( X X. X ) <-> E. x e. X E. y e. X p = <. x , y >. )
24 23 bilani 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> E. x e. X E. y e. X p = <. x , y >. )
25 simpr 
 |-  ( ( ph /\ p = <. x , y >. ) -> p = <. x , y >. )
26 25 eleq1d 
 |-  ( ( ph /\ p = <. x , y >. ) -> ( p e. r <-> <. x , y >. e. r ) )
27 26 adantlr 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( p e. r <-> <. x , y >. e. r ) )
28 df-br 
 |-  ( x r y <-> <. x , y >. e. r )
29 27 28 bitr4di 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( p e. r <-> x r y ) )
30 simplr 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> p e. ( X X. X ) )
31 opex 
 |-  <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. e. _V
32 1 2 3 4 5 ucnimalem 
 |-  G = ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
33 32 fvmpt2 
 |-  ( ( p e. ( X X. X ) /\ <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. e. _V ) -> ( G ` p ) = <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
34 30 31 33 sylancl 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( G ` p ) = <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
35 simpr 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> p = <. x , y >. )
36 1st2nd2 
 |-  ( p e. ( X X. X ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
37 30 36 syl 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
38 35 37 eqtr3d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> <. x , y >. = <. ( 1st ` p ) , ( 2nd ` p ) >. )
39 vex 
 |-  x e. _V
40 vex 
 |-  y e. _V
41 39 40 opth 
 |-  ( <. x , y >. = <. ( 1st ` p ) , ( 2nd ` p ) >. <-> ( x = ( 1st ` p ) /\ y = ( 2nd ` p ) ) )
42 38 41 sylib 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( x = ( 1st ` p ) /\ y = ( 2nd ` p ) ) )
43 42 simpld 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> x = ( 1st ` p ) )
44 43 fveq2d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( F ` x ) = ( F ` ( 1st ` p ) ) )
45 42 simprd 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> y = ( 2nd ` p ) )
46 45 fveq2d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( F ` y ) = ( F ` ( 2nd ` p ) ) )
47 44 46 opeq12d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> <. ( F ` x ) , ( F ` y ) >. = <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
48 34 47 eqtr4d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( G ` p ) = <. ( F ` x ) , ( F ` y ) >. )
49 48 eleq1d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( ( G ` p ) e. W <-> <. ( F ` x ) , ( F ` y ) >. e. W ) )
50 df-br 
 |-  ( ( F ` x ) W ( F ` y ) <-> <. ( F ` x ) , ( F ` y ) >. e. W )
51 49 50 bitr4di 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( ( G ` p ) e. W <-> ( F ` x ) W ( F ` y ) ) )
52 29 51 imbi12d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( ( p e. r -> ( G ` p ) e. W ) <-> ( x r y -> ( F ` x ) W ( F ` y ) ) ) )
53 52 exbiri 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> ( p = <. x , y >. -> ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) )
54 53 reximdv 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> ( E. y e. X p = <. x , y >. -> E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) )
55 54 reximdv 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> ( E. x e. X E. y e. X p = <. x , y >. -> E. x e. X E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) )
56 24 55 mpd 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> E. x e. X E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) )
57 56 adantlr 
 |-  ( ( ( ph /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. ( X X. X ) ) -> E. x e. X E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) )
58 22 57 r19.29d2r 
 |-  ( ( ( ph /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. ( X X. X ) ) -> E. x e. X E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) /\ ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) )
59 pm3.35 
 |-  ( ( ( x r y -> ( F ` x ) W ( F ` y ) ) /\ ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) -> ( p e. r -> ( G ` p ) e. W ) )
60 59 rexlimivw 
 |-  ( E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) /\ ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) -> ( p e. r -> ( G ` p ) e. W ) )
61 60 rexlimivw 
 |-  ( E. x e. X E. y e. X ( ( x r y -> ( F ` x ) W ( F ` y ) ) /\ ( ( x r y -> ( F ` x ) W ( F ` y ) ) -> ( p e. r -> ( G ` p ) e. W ) ) ) -> ( p e. r -> ( G ` p ) e. W ) )
62 58 61 syl 
 |-  ( ( ( ph /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. ( X X. X ) ) -> ( p e. r -> ( G ` p ) e. W ) )
63 62 imp 
 |-  ( ( ( ( ph /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. ( X X. X ) ) /\ p e. r ) -> ( G ` p ) e. W )
64 15 16 20 21 63 syl1111anc 
 |-  ( ( ( ( ph /\ r e. U ) /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) /\ p e. r ) -> ( G ` p ) e. W )
65 64 ralrimiva 
 |-  ( ( ( ph /\ r e. U ) /\ A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) ) -> A. p e. r ( G ` p ) e. W )
66 65 ex 
 |-  ( ( ph /\ r e. U ) -> ( A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) -> A. p e. r ( G ` p ) e. W ) )
67 66 reximdva 
 |-  ( ph -> ( E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) W ( F ` y ) ) -> E. r e. U A. p e. r ( G ` p ) e. W ) )
68 14 67 mpd 
 |-  ( ph -> E. r e. U A. p e. r ( G ` p ) e. W )
69 5 mpofun 
 |-  Fun G
70 opex 
 |-  <. ( F ` x ) , ( F ` y ) >. e. _V
71 5 70 dmmpo 
 |-  dom G = ( X X. X )
72 18 71 sseqtrrdi 
 |-  ( ( ph /\ r e. U ) -> r C_ dom G )
73 funimass4 
 |-  ( ( Fun G /\ r C_ dom G ) -> ( ( G " r ) C_ W <-> A. p e. r ( G ` p ) e. W ) )
74 69 72 73 sylancr 
 |-  ( ( ph /\ r e. U ) -> ( ( G " r ) C_ W <-> A. p e. r ( G ` p ) e. W ) )
75 74 biimprd 
 |-  ( ( ph /\ r e. U ) -> ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) )
76 75 ralrimiva 
 |-  ( ph -> A. r e. U ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) )
77 r19.29r 
 |-  ( ( E. r e. U A. p e. r ( G ` p ) e. W /\ A. r e. U ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) ) -> E. r e. U ( A. p e. r ( G ` p ) e. W /\ ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) ) )
78 68 76 77 syl2anc 
 |-  ( ph -> E. r e. U ( A. p e. r ( G ` p ) e. W /\ ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) ) )
79 pm3.35 
 |-  ( ( A. p e. r ( G ` p ) e. W /\ ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) ) -> ( G " r ) C_ W )
80 79 reximi 
 |-  ( E. r e. U ( A. p e. r ( G ` p ) e. W /\ ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) ) -> E. r e. U ( G " r ) C_ W )
81 78 80 syl 
 |-  ( ph -> E. r e. U ( G " r ) C_ W )