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 simpr 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> p e. ( X X. X ) )
24 elxp2 
 |-  ( p e. ( X X. X ) <-> E. x e. X E. y e. X p = <. x , y >. )
25 23 24 sylib 
 |-  ( ( ph /\ p e. ( X X. X ) ) -> E. x e. X E. y e. X p = <. x , y >. )
26 simpr 
 |-  ( ( ph /\ p = <. x , y >. ) -> p = <. x , y >. )
27 26 eleq1d 
 |-  ( ( ph /\ p = <. x , y >. ) -> ( p e. r <-> <. x , y >. e. r ) )
28 27 adantlr 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( p e. r <-> <. x , y >. e. r ) )
29 df-br 
 |-  ( x r y <-> <. x , y >. e. r )
30 28 29 bitr4di 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( p e. r <-> x r y ) )
31 simplr 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> p e. ( X X. X ) )
32 opex 
 |-  <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. e. _V
33 1 2 3 4 5 ucnimalem 
 |-  G = ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
34 33 fvmpt2 
 |-  ( ( p e. ( X X. X ) /\ <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. e. _V ) -> ( G ` p ) = <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
35 31 32 34 sylancl 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( G ` p ) = <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
36 simpr 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> p = <. x , y >. )
37 1st2nd2 
 |-  ( p e. ( X X. X ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
38 31 37 syl 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
39 36 38 eqtr3d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> <. x , y >. = <. ( 1st ` p ) , ( 2nd ` p ) >. )
40 vex 
 |-  x e. _V
41 vex 
 |-  y e. _V
42 40 41 opth 
 |-  ( <. x , y >. = <. ( 1st ` p ) , ( 2nd ` p ) >. <-> ( x = ( 1st ` p ) /\ y = ( 2nd ` p ) ) )
43 39 42 sylib 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( x = ( 1st ` p ) /\ y = ( 2nd ` p ) ) )
44 43 simpld 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> x = ( 1st ` p ) )
45 44 fveq2d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( F ` x ) = ( F ` ( 1st ` p ) ) )
46 43 simprd 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> y = ( 2nd ` p ) )
47 46 fveq2d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( F ` y ) = ( F ` ( 2nd ` p ) ) )
48 45 47 opeq12d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> <. ( F ` x ) , ( F ` y ) >. = <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
49 35 48 eqtr4d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( G ` p ) = <. ( F ` x ) , ( F ` y ) >. )
50 49 eleq1d 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( ( G ` p ) e. W <-> <. ( F ` x ) , ( F ` y ) >. e. W ) )
51 df-br 
 |-  ( ( F ` x ) W ( F ` y ) <-> <. ( F ` x ) , ( F ` y ) >. e. W )
52 50 51 bitr4di 
 |-  ( ( ( ph /\ p e. ( X X. X ) ) /\ p = <. x , y >. ) -> ( ( G ` p ) e. W <-> ( F ` x ) W ( F ` y ) ) )
53 30 52 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 ) ) ) )
54 53 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 ) ) ) )
55 54 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 ) ) ) )
56 55 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 ) ) ) )
57 25 56 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 ) ) )
58 57 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 ) ) )
59 22 58 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 ) ) ) )
60 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 ) )
61 60 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 ) )
62 61 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 ) )
63 59 62 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 ) )
64 63 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 )
65 15 16 20 21 64 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 )
66 65 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 )
67 66 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 ) )
68 67 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 ) )
69 14 68 mpd 
 |-  ( ph -> E. r e. U A. p e. r ( G ` p ) e. W )
70 5 mpofun 
 |-  Fun G
71 opex 
 |-  <. ( F ` x ) , ( F ` y ) >. e. _V
72 5 71 dmmpo 
 |-  dom G = ( X X. X )
73 18 72 sseqtrrdi 
 |-  ( ( ph /\ r e. U ) -> r C_ dom G )
74 funimass4 
 |-  ( ( Fun G /\ r C_ dom G ) -> ( ( G " r ) C_ W <-> A. p e. r ( G ` p ) e. W ) )
75 70 73 74 sylancr 
 |-  ( ( ph /\ r e. U ) -> ( ( G " r ) C_ W <-> A. p e. r ( G ` p ) e. W ) )
76 75 biimprd 
 |-  ( ( ph /\ r e. U ) -> ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) )
77 76 ralrimiva 
 |-  ( ph -> A. r e. U ( A. p e. r ( G ` p ) e. W -> ( G " r ) C_ W ) )
78 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 ) ) )
79 69 77 78 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 ) ) )
80 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 )
81 80 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 )
82 79 81 syl 
 |-  ( ph -> E. r e. U ( G " r ) C_ W )