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
|- ( J e. ( TopOn ` X ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> J ~~ 2o )
2 toponss
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
3 2 ad2ant2rl
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> x C_ X )
4 simprl
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> X = (/) )
5 sseq0
 |-  ( ( x C_ X /\ X = (/) ) -> x = (/) )
6 3 4 5 syl2anc
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> x = (/) )
7 velsn
 |-  ( x e. { (/) } <-> x = (/) )
8 6 7 sylibr
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> x e. { (/) } )
9 8 expr
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> ( x e. J -> x e. { (/) } ) )
10 9 ssrdv
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J C_ { (/) } )
11 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
12 0opn
 |-  ( J e. Top -> (/) e. J )
13 11 12 syl
 |-  ( J e. ( TopOn ` X ) -> (/) e. J )
14 13 ad2antrr
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> (/) e. J )
15 14 snssd
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> { (/) } C_ J )
16 10 15 eqssd
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J = { (/) } )
17 0ex
 |-  (/) e. _V
18 17 ensn1
 |-  { (/) } ~~ 1o
19 16 18 eqbrtrdi
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J ~~ 1o )
20 19 olcd
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> ( J = (/) \/ J ~~ 1o ) )
21 sdom2en01
 |-  ( J ~< 2o <-> ( J = (/) \/ J ~~ 1o ) )
22 20 21 sylibr
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J ~< 2o )
23 sdomnen
 |-  ( J ~< 2o -> -. J ~~ 2o )
24 22 23 syl
 |-  ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> -. J ~~ 2o )
25 24 ex
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( X = (/) -> -. J ~~ 2o ) )
26 25 necon2ad
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( J ~~ 2o -> X =/= (/) ) )
27 1 26 mpd
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> X =/= (/) )
28 27 necomd
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> (/) =/= X )
29 13 adantr
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> (/) e. J )
30 toponmax
 |-  ( J e. ( TopOn ` X ) -> X e. J )
31 30 adantr
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> X e. J )
32 en2eqpr
 |-  ( ( J ~~ 2o /\ (/) e. J /\ X e. J ) -> ( (/) =/= X -> J = { (/) , X } ) )
33 1 29 31 32 syl3anc
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( (/) =/= X -> J = { (/) , X } ) )
34 28 33 mpd
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> J = { (/) , X } )
35 34 27 jca
 |-  ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( J = { (/) , X } /\ X =/= (/) ) )
36 simprl
 |-  ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> J = { (/) , X } )
37 simprr
 |-  ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> X =/= (/) )
38 37 necomd
 |-  ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> (/) =/= X )
39 pr2nelem
 |-  ( ( (/) e. _V /\ X e. J /\ (/) =/= X ) -> { (/) , X } ~~ 2o )
40 17 30 38 39 mp3an2ani
 |-  ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> { (/) , X } ~~ 2o )
41 36 40 eqbrtrd
 |-  ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> J ~~ 2o )
42 35 41 impbida
 |-  ( J e. ( TopOn ` X ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )