This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )