Metamath Proof Explorer


Theorem ucnprima

Description: The preimage by a uniformly continuous function F of an entourage W of Y is an entourage of X . Note of the definition 1 of BourbakiTop1 p. II.6. (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 ucnprima
|- ( ph -> ( `' G " W ) e. U )

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 1 2 3 4 5 ucnima
 |-  ( ph -> E. r e. U ( G " r ) C_ W )
7 5 mpofun
 |-  Fun G
8 ustssxp
 |-  ( ( U e. ( UnifOn ` X ) /\ r e. U ) -> r C_ ( X X. X ) )
9 1 8 sylan
 |-  ( ( ph /\ r e. U ) -> r C_ ( X X. X ) )
10 opex
 |-  <. ( F ` x ) , ( F ` y ) >. e. _V
11 5 10 dmmpo
 |-  dom G = ( X X. X )
12 9 11 sseqtrrdi
 |-  ( ( ph /\ r e. U ) -> r C_ dom G )
13 funimass3
 |-  ( ( Fun G /\ r C_ dom G ) -> ( ( G " r ) C_ W <-> r C_ ( `' G " W ) ) )
14 7 12 13 sylancr
 |-  ( ( ph /\ r e. U ) -> ( ( G " r ) C_ W <-> r C_ ( `' G " W ) ) )
15 14 rexbidva
 |-  ( ph -> ( E. r e. U ( G " r ) C_ W <-> E. r e. U r C_ ( `' G " W ) ) )
16 6 15 mpbid
 |-  ( ph -> E. r e. U r C_ ( `' G " W ) )
17 1 adantr
 |-  ( ( ph /\ r e. U ) -> U e. ( UnifOn ` X ) )
18 simpr
 |-  ( ( ph /\ r e. U ) -> r e. U )
19 cnvimass
 |-  ( `' G " W ) C_ dom G
20 19 11 sseqtri
 |-  ( `' G " W ) C_ ( X X. X )
21 20 a1i
 |-  ( ( ph /\ r e. U ) -> ( `' G " W ) C_ ( X X. X ) )
22 ustssel
 |-  ( ( U e. ( UnifOn ` X ) /\ r e. U /\ ( `' G " W ) C_ ( X X. X ) ) -> ( r C_ ( `' G " W ) -> ( `' G " W ) e. U ) )
23 17 18 21 22 syl3anc
 |-  ( ( ph /\ r e. U ) -> ( r C_ ( `' G " W ) -> ( `' G " W ) e. U ) )
24 23 rexlimdva
 |-  ( ph -> ( E. r e. U r C_ ( `' G " W ) -> ( `' G " W ) e. U ) )
25 16 24 mpd
 |-  ( ph -> ( `' G " W ) e. U )