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 enpr2 
 |-  ( ( (/) 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 =/= (/) ) ) )