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