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 φ U UnifOn X
ucnprima.2 φ V UnifOn Y
ucnprima.3 φ F U uCn V
ucnprima.4 φ W V
ucnprima.5 G = x X , y X F x F y
Assertion ucnima φ r U G r W

Proof

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