Metamath Proof Explorer


Theorem en2top

Description: If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion en2top JTopOnXJ2𝑜J=XX

Proof

Step Hyp Ref Expression
1 simpr JTopOnXJ2𝑜J2𝑜
2 toponss JTopOnXxJxX
3 2 ad2ant2rl JTopOnXJ2𝑜X=xJxX
4 simprl JTopOnXJ2𝑜X=xJX=
5 sseq0 xXX=x=
6 3 4 5 syl2anc JTopOnXJ2𝑜X=xJx=
7 velsn xx=
8 6 7 sylibr JTopOnXJ2𝑜X=xJx
9 8 expr JTopOnXJ2𝑜X=xJx
10 9 ssrdv JTopOnXJ2𝑜X=J
11 topontop JTopOnXJTop
12 0opn JTopJ
13 11 12 syl JTopOnXJ
14 13 ad2antrr JTopOnXJ2𝑜X=J
15 14 snssd JTopOnXJ2𝑜X=J
16 10 15 eqssd JTopOnXJ2𝑜X=J=
17 0ex V
18 17 ensn1 1𝑜
19 16 18 eqbrtrdi JTopOnXJ2𝑜X=J1𝑜
20 19 olcd JTopOnXJ2𝑜X=J=J1𝑜
21 sdom2en01 J2𝑜J=J1𝑜
22 20 21 sylibr JTopOnXJ2𝑜X=J2𝑜
23 sdomnen J2𝑜¬J2𝑜
24 22 23 syl JTopOnXJ2𝑜X=¬J2𝑜
25 24 ex JTopOnXJ2𝑜X=¬J2𝑜
26 25 necon2ad JTopOnXJ2𝑜J2𝑜X
27 1 26 mpd JTopOnXJ2𝑜X
28 27 necomd JTopOnXJ2𝑜X
29 13 adantr JTopOnXJ2𝑜J
30 toponmax JTopOnXXJ
31 30 adantr JTopOnXJ2𝑜XJ
32 en2eqpr J2𝑜JXJXJ=X
33 1 29 31 32 syl3anc JTopOnXJ2𝑜XJ=X
34 28 33 mpd JTopOnXJ2𝑜J=X
35 34 27 jca JTopOnXJ2𝑜J=XX
36 simprl JTopOnXJ=XXJ=X
37 simprr JTopOnXJ=XXX
38 37 necomd JTopOnXJ=XXX
39 pr2nelem VXJXX2𝑜
40 17 30 38 39 mp3an2ani JTopOnXJ=XXX2𝑜
41 36 40 eqbrtrd JTopOnXJ=XXJ2𝑜
42 35 41 impbida JTopOnXJ2𝑜J=XX