Metamath Proof Explorer

Theorem ssidcn

Description: The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion ssidcn 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> K C_ J ) )

Proof

Step Hyp Ref Expression
1 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> ( ( _I |` X ) : X --> X /\ A. x e. K ( `' ( _I |` X ) " x ) e. J ) ) )
2 f1oi 
 |-  ( _I |` X ) : X -1-1-onto-> X
3 f1of 
 |-  ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X --> X )
4 2 3 ax-mp 
 |-  ( _I |` X ) : X --> X
5 4 biantrur 
 |-  ( A. x e. K ( `' ( _I |` X ) " x ) e. J <-> ( ( _I |` X ) : X --> X /\ A. x e. K ( `' ( _I |` X ) " x ) e. J ) )
6 1 5 bitr4di 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> A. x e. K ( `' ( _I |` X ) " x ) e. J ) )
7 cnvresid 
 |-  `' ( _I |` X ) = ( _I |` X )
8 7 imaeq1i 
 |-  ( `' ( _I |` X ) " x ) = ( ( _I |` X ) " x )
9 elssuni 
 |-  ( x e. K -> x C_ U. K )
10 9 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> x C_ U. K )
11 toponuni 
 |-  ( K e. ( TopOn ` X ) -> X = U. K )
12 11 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> X = U. K )
13 10 12 sseqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> x C_ X )
14 resiima 
 |-  ( x C_ X -> ( ( _I |` X ) " x ) = x )
15 13 14 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> ( ( _I |` X ) " x ) = x )
16 8 15 syl5eq 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> ( `' ( _I |` X ) " x ) = x )
17 16 eleq1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> ( ( `' ( _I |` X ) " x ) e. J <-> x e. J ) )
18 17 ralbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( A. x e. K ( `' ( _I |` X ) " x ) e. J <-> A. x e. K x e. J ) )
19 dfss3 
 |-  ( K C_ J <-> A. x e. K x e. J )
20 18 19 bitr4di 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( A. x e. K ( `' ( _I |` X ) " x ) e. J <-> K C_ J ) )
21 6 20 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> K C_ J ) )