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 )

Metamath Proof Explorer

Theorem ucnprima

Proof