Metamath Proof Explorer


Theorem cnindis

Description: Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnindis J TopOn X A V J Cn A = A X

Proof

Step Hyp Ref Expression
1 elpri x A x = x = A
2 topontop J TopOn X J Top
3 2 ad2antrr J TopOn X A V f : X A J Top
4 0opn J Top J
5 3 4 syl J TopOn X A V f : X A J
6 imaeq2 x = f -1 x = f -1
7 ima0 f -1 =
8 6 7 eqtrdi x = f -1 x =
9 8 eleq1d x = f -1 x J J
10 5 9 syl5ibrcom J TopOn X A V f : X A x = f -1 x J
11 fimacnv f : X A f -1 A = X
12 11 adantl J TopOn X A V f : X A f -1 A = X
13 toponmax J TopOn X X J
14 13 ad2antrr J TopOn X A V f : X A X J
15 12 14 eqeltrd J TopOn X A V f : X A f -1 A J
16 imaeq2 x = A f -1 x = f -1 A
17 16 eleq1d x = A f -1 x J f -1 A J
18 15 17 syl5ibrcom J TopOn X A V f : X A x = A f -1 x J
19 10 18 jaod J TopOn X A V f : X A x = x = A f -1 x J
20 1 19 syl5 J TopOn X A V f : X A x A f -1 x J
21 20 ralrimiv J TopOn X A V f : X A x A f -1 x J
22 21 ex J TopOn X A V f : X A x A f -1 x J
23 22 pm4.71d J TopOn X A V f : X A f : X A x A f -1 x J
24 id A V A V
25 elmapg A V X J f A X f : X A
26 24 13 25 syl2anr J TopOn X A V f A X f : X A
27 indistopon A V A TopOn A
28 iscn J TopOn X A TopOn A f J Cn A f : X A x A f -1 x J
29 27 28 sylan2 J TopOn X A V f J Cn A f : X A x A f -1 x J
30 23 26 29 3bitr4rd J TopOn X A V f J Cn A f A X
31 30 eqrdv J TopOn X A V J Cn A = A X