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 JTopOnXAVJCnA=AX

Proof

Step Hyp Ref Expression
1 elpri xAx=x=A
2 topontop JTopOnXJTop
3 2 ad2antrr JTopOnXAVf:XAJTop
4 0opn JTopJ
5 3 4 syl JTopOnXAVf:XAJ
6 imaeq2 x=f-1x=f-1
7 ima0 f-1=
8 6 7 eqtrdi x=f-1x=
9 8 eleq1d x=f-1xJJ
10 5 9 syl5ibrcom JTopOnXAVf:XAx=f-1xJ
11 fimacnv f:XAf-1A=X
12 11 adantl JTopOnXAVf:XAf-1A=X
13 toponmax JTopOnXXJ
14 13 ad2antrr JTopOnXAVf:XAXJ
15 12 14 eqeltrd JTopOnXAVf:XAf-1AJ
16 imaeq2 x=Af-1x=f-1A
17 16 eleq1d x=Af-1xJf-1AJ
18 15 17 syl5ibrcom JTopOnXAVf:XAx=Af-1xJ
19 10 18 jaod JTopOnXAVf:XAx=x=Af-1xJ
20 1 19 syl5 JTopOnXAVf:XAxAf-1xJ
21 20 ralrimiv JTopOnXAVf:XAxAf-1xJ
22 21 ex JTopOnXAVf:XAxAf-1xJ
23 22 pm4.71d JTopOnXAVf:XAf:XAxAf-1xJ
24 id AVAV
25 elmapg AVXJfAXf:XA
26 24 13 25 syl2anr JTopOnXAVfAXf:XA
27 indistopon AVATopOnA
28 iscn JTopOnXATopOnAfJCnAf:XAxAf-1xJ
29 27 28 sylan2 JTopOnXAVfJCnAf:XAxAf-1xJ
30 23 26 29 3bitr4rd JTopOnXAVfJCnAfAX
31 30 eqrdv JTopOnXAVJCnA=AX