Metamath Proof Explorer

Theorem en1top

Description: { (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008)

Ref Expression
Assertion en1top 
|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )

Proof

Step Hyp Ref Expression
1 0opn 
 |-  ( J e. Top -> (/) e. J )
2 en1eqsn 
 |-  ( ( (/) e. J /\ J ~~ 1o ) -> J = { (/) } )
3 2 ex 
 |-  ( (/) e. J -> ( J ~~ 1o -> J = { (/) } ) )
4 1 3 syl 
 |-  ( J e. Top -> ( J ~~ 1o -> J = { (/) } ) )
5 id 
 |-  ( J = { (/) } -> J = { (/) } )
6 0ex 
 |-  (/) e. _V
7 6 ensn1 
 |-  { (/) } ~~ 1o
8 5 7 eqbrtrdi 
 |-  ( J = { (/) } -> J ~~ 1o )
9 4 8 impbid1 
 |-  ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )