Metamath Proof Explorer

Theorem isucn2

Description: The predicate " F is a uniformly continuous function from uniform space U to uniform space V ", expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018)

Ref Expression
Hypotheses isucn2.u 
|- U = ( ( X X. X ) filGen R )
isucn2.v 
|- V = ( ( Y X. Y ) filGen S )
isucn2.1 
|- ( ph -> U e. ( UnifOn ` X ) )
isucn2.2 
|- ( ph -> V e. ( UnifOn ` Y ) )
isucn2.3 
|- ( ph -> R e. ( fBas ` ( X X. X ) ) )
isucn2.4 
|- ( ph -> S e. ( fBas ` ( Y X. Y ) ) )
Assertion isucn2 
|- ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isucn2.u 
 |-  U = ( ( X X. X ) filGen R )
2 isucn2.v 
 |-  V = ( ( Y X. Y ) filGen S )
3 isucn2.1 
 |-  ( ph -> U e. ( UnifOn ` X ) )
4 isucn2.2 
 |-  ( ph -> V e. ( UnifOn ` Y ) )
5 isucn2.3 
 |-  ( ph -> R e. ( fBas ` ( X X. X ) ) )
6 isucn2.4 
 |-  ( ph -> S e. ( fBas ` ( Y X. Y ) ) )
7 isucn 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) ) )
8 3 4 7 syl2anc 
 |-  ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) ) )
9 breq 
 |-  ( v = s -> ( ( F ` x ) v ( F ` y ) <-> ( F ` x ) s ( F ` y ) ) )
10 9 imbi2d 
 |-  ( v = s -> ( ( x u y -> ( F ` x ) v ( F ` y ) ) <-> ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
11 10 ralbidv 
 |-  ( v = s -> ( A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
12 11 rexralbidv 
 |-  ( v = s -> ( E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
13 simplr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) /\ s e. S ) -> A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) )
14 ssfg 
 |-  ( S e. ( fBas ` ( Y X. Y ) ) -> S C_ ( ( Y X. Y ) filGen S ) )
15 6 14 syl 
 |-  ( ph -> S C_ ( ( Y X. Y ) filGen S ) )
16 15 2 sseqtrrdi 
 |-  ( ph -> S C_ V )
17 16 adantr 
 |-  ( ( ph /\ F : X --> Y ) -> S C_ V )
18 17 adantr 
 |-  ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) -> S C_ V )
19 18 sselda 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) /\ s e. S ) -> s e. V )
20 12 13 19 rspcdva 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) /\ s e. S ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) )
21 simpr 
 |-  ( ( ph /\ u e. U ) -> u e. U )
22 21 1 eleqtrdi 
 |-  ( ( ph /\ u e. U ) -> u e. ( ( X X. X ) filGen R ) )
23 elfg 
 |-  ( R e. ( fBas ` ( X X. X ) ) -> ( u e. ( ( X X. X ) filGen R ) <-> ( u C_ ( X X. X ) /\ E. r e. R r C_ u ) ) )
24 5 23 syl 
 |-  ( ph -> ( u e. ( ( X X. X ) filGen R ) <-> ( u C_ ( X X. X ) /\ E. r e. R r C_ u ) ) )
25 24 simplbda 
 |-  ( ( ph /\ u e. ( ( X X. X ) filGen R ) ) -> E. r e. R r C_ u )
26 22 25 syldan 
 |-  ( ( ph /\ u e. U ) -> E. r e. R r C_ u )
27 ssbr 
 |-  ( r C_ u -> ( x r y -> x u y ) )
28 27 imim1d 
 |-  ( r C_ u -> ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
29 28 adantl 
 |-  ( ( ( ph /\ r e. R ) /\ r C_ u ) -> ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
30 29 ralrimivw 
 |-  ( ( ( ph /\ r e. R ) /\ r C_ u ) -> A. y e. X ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
31 30 ralrimivw 
 |-  ( ( ( ph /\ r e. R ) /\ r C_ u ) -> A. x e. X A. y e. X ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
32 ralim 
 |-  ( A. y e. X ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x r y -> ( F ` x ) s ( F ` y ) ) ) -> ( A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
33 32 ralimi 
 |-  ( A. x e. X A. y e. X ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x r y -> ( F ` x ) s ( F ` y ) ) ) -> A. x e. X ( A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
34 ralim 
 |-  ( A. x e. X ( A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
35 31 33 34 3syl 
 |-  ( ( ( ph /\ r e. R ) /\ r C_ u ) -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
36 35 ex 
 |-  ( ( ph /\ r e. R ) -> ( r C_ u -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )
37 36 reximdva 
 |-  ( ph -> ( E. r e. R r C_ u -> E. r e. R ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )
38 37 adantr 
 |-  ( ( ph /\ u e. U ) -> ( E. r e. R r C_ u -> E. r e. R ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )
39 26 38 mpd 
 |-  ( ( ph /\ u e. U ) -> E. r e. R ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
40 r19.37v 
 |-  ( E. r e. R ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
41 39 40 syl 
 |-  ( ( ph /\ u e. U ) -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
42 41 rexlimdva 
 |-  ( ph -> ( E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
43 42 ad3antrrr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) /\ s e. S ) -> ( E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
44 20 43 mpd 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) /\ s e. S ) -> E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) )
45 44 ralrimiva 
 |-  ( ( ( ph /\ F : X --> Y ) /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) -> A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) )
46 ssfg 
 |-  ( R e. ( fBas ` ( X X. X ) ) -> R C_ ( ( X X. X ) filGen R ) )
47 5 46 syl 
 |-  ( ph -> R C_ ( ( X X. X ) filGen R ) )
48 47 1 sseqtrrdi 
 |-  ( ph -> R C_ U )
49 ssrexv 
 |-  ( R C_ U -> ( E. r e. R 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 ) ) ) )
50 breq 
 |-  ( r = u -> ( x r y <-> x u y ) )
51 50 imbi1d 
 |-  ( r = u -> ( ( x r y -> ( F ` x ) s ( F ` y ) ) <-> ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
52 51 2ralbidv 
 |-  ( r = u -> ( A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) <-> A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
53 52 cbvrexvw 
 |-  ( E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) <-> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) )
54 49 53 syl6ib 
 |-  ( R C_ U -> ( E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
55 48 54 syl 
 |-  ( ph -> ( E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
56 55 ralimdv 
 |-  ( ph -> ( A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) -> A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
57 56 adantr 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) -> A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) )
58 nfv 
 |-  F/ s ( ph /\ F : X --> Y )
59 nfra1 
 |-  F/ s A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) )
60 58 59 nfan 
 |-  F/ s ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) )
61 nfv 
 |-  F/ s v e. V
62 60 61 nfan 
 |-  F/ s ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V )
63 rspa 
 |-  ( ( A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) /\ s e. S ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) )
64 63 ad5ant24 
 |-  ( ( ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) /\ s e. S ) /\ s C_ v ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) )
65 simp-4l 
 |-  ( ( ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) /\ s e. S ) /\ s C_ v ) -> ( ph /\ F : X --> Y ) )
66 simplr 
 |-  ( ( ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) /\ s e. S ) /\ s C_ v ) -> s e. S )
67 simpr 
 |-  ( ( ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) /\ s e. S ) /\ s C_ v ) -> s C_ v )
68 ssbr 
 |-  ( s C_ v -> ( ( F ` x ) s ( F ` y ) -> ( F ` x ) v ( F ` y ) ) )
69 68 adantl 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ s e. S ) /\ s C_ v ) -> ( ( F ` x ) s ( F ` y ) -> ( F ` x ) v ( F ` y ) ) )
70 69 imim2d 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ s e. S ) /\ s C_ v ) -> ( ( x u y -> ( F ` x ) s ( F ` y ) ) -> ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
71 70 ralimdv 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ s e. S ) /\ s C_ v ) -> ( A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
72 71 ralimdv 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ s e. S ) /\ s C_ v ) -> ( A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
73 72 reximdv 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ s e. S ) /\ s C_ v ) -> ( E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
74 65 66 67 73 syl21anc 
 |-  ( ( ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) /\ s e. S ) /\ s C_ v ) -> ( E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
75 64 74 mpd 
 |-  ( ( ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) /\ s e. S ) /\ s C_ v ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) )
76 6 ad3antrrr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) -> S e. ( fBas ` ( Y X. Y ) ) )
77 simpr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) -> v e. V )
78 77 2 eleqtrdi 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) -> v e. ( ( Y X. Y ) filGen S ) )
79 elfg 
 |-  ( S e. ( fBas ` ( Y X. Y ) ) -> ( v e. ( ( Y X. Y ) filGen S ) <-> ( v C_ ( Y X. Y ) /\ E. s e. S s C_ v ) ) )
80 79 simplbda 
 |-  ( ( S e. ( fBas ` ( Y X. Y ) ) /\ v e. ( ( Y X. Y ) filGen S ) ) -> E. s e. S s C_ v )
81 76 78 80 syl2anc 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) -> E. s e. S s C_ v )
82 62 75 81 r19.29af 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) /\ v e. V ) -> E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) )
83 82 ralrimiva 
 |-  ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) ) -> A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) )
84 83 ex 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. s e. S E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) s ( F ` y ) ) -> A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
85 57 84 syld 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) -> A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) )
86 85 imp 
 |-  ( ( ( ph /\ F : X --> Y ) /\ A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) -> A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) )
87 45 86 impbida 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) <-> A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) )
88 87 pm5.32da 
 |-  ( ph -> ( ( F : X --> Y /\ A. v e. V E. u e. U A. x e. X A. y e. X ( x u y -> ( F ` x ) v ( F ` y ) ) ) <-> ( F : X --> Y /\ A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )
89 8 88 bitrd 
 |-  ( ph -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )