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

Metamath Proof Explorer

Theorem iducn

Description: The identity is uniformly continuous from a uniform structure to itself. Example 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion iducn 
|- ( U e. ( UnifOn ` X ) -> ( _I |` X ) e. ( U uCn U ) )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` X ) : X -1-1-onto-> X
2 f1of 
 |-  ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X --> X )
3 1 2 mp1i 
 |-  ( U e. ( UnifOn ` X ) -> ( _I |` X ) : X --> X )
4 simpr 
 |-  ( ( U e. ( UnifOn ` X ) /\ s e. U ) -> s e. U )
5 fvresi 
 |-  ( x e. X -> ( ( _I |` X ) ` x ) = x )
6 fvresi 
 |-  ( y e. X -> ( ( _I |` X ) ` y ) = y )
7 5 6 breqan12d 
 |-  ( ( x e. X /\ y e. X ) -> ( ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) <-> x s y ) )
8 7 biimprd 
 |-  ( ( x e. X /\ y e. X ) -> ( x s y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) )
9 8 adantl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ s e. U ) /\ ( x e. X /\ y e. X ) ) -> ( x s y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) )
10 9 ralrimivva 
 |-  ( ( U e. ( UnifOn ` X ) /\ s e. U ) -> A. x e. X A. y e. X ( x s y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) )
11 breq 
 |-  ( r = s -> ( x r y <-> x s y ) )
12 11 imbi1d 
 |-  ( r = s -> ( ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) <-> ( x s y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) ) )
13 12 2ralbidv 
 |-  ( r = s -> ( A. x e. X A. y e. X ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) <-> A. x e. X A. y e. X ( x s y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) ) )
14 13 rspcev 
 |-  ( ( s e. U /\ A. x e. X A. y e. X ( x s y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) ) -> E. r e. U A. x e. X A. y e. X ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) )
15 4 10 14 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ s e. U ) -> E. r e. U A. x e. X A. y e. X ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) )
16 15 ralrimiva 
 |-  ( U e. ( UnifOn ` X ) -> A. s e. U E. r e. U A. x e. X A. y e. X ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) )
17 isucn 
 |-  ( ( U e. ( UnifOn ` X ) /\ U e. ( UnifOn ` X ) ) -> ( ( _I |` X ) e. ( U uCn U ) <-> ( ( _I |` X ) : X --> X /\ A. s e. U E. r e. U A. x e. X A. y e. X ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) ) ) )
18 17 anidms 
 |-  ( U e. ( UnifOn ` X ) -> ( ( _I |` X ) e. ( U uCn U ) <-> ( ( _I |` X ) : X --> X /\ A. s e. U E. r e. U A. x e. X A. y e. X ( x r y -> ( ( _I |` X ) ` x ) s ( ( _I |` X ) ` y ) ) ) ) )
19 3 16 18 mpbir2and 
 |-  ( U e. ( UnifOn ` X ) -> ( _I |` X ) e. ( U uCn U ) )