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 TopOn X K TopOn X I X J Cn K K J

Proof

Step Hyp Ref Expression
1 iscn J TopOn X K TopOn X I X J Cn K I X : X X x K I X -1 x 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 x K I X -1 x J I X : X X x K I X -1 x J
6 1 5 bitr4di J TopOn X K TopOn X I X J Cn K x K I X -1 x J
7 cnvresid I X -1 = I X
8 7 imaeq1i I X -1 x = I X x
9 elssuni x K x K
10 9 adantl J TopOn X K TopOn X x K x K
11 toponuni K TopOn X X = K
12 11 ad2antlr J TopOn X K TopOn X x K X = K
13 10 12 sseqtrrd J TopOn X K TopOn X x K x X
14 resiima x X I X x = x
15 13 14 syl J TopOn X K TopOn X x K I X x = x
16 8 15 syl5eq J TopOn X K TopOn X x K I X -1 x = x
17 16 eleq1d J TopOn X K TopOn X x K I X -1 x J x J
18 17 ralbidva J TopOn X K TopOn X x K I X -1 x J x K x J
19 dfss3 K J x K x J
20 18 19 bitr4di J TopOn X K TopOn X x K I X -1 x J K J
21 6 20 bitrd J TopOn X K TopOn X I X J Cn K K J