Metamath Proof Explorer


Theorem 0top

Description: The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006)

Ref Expression
Assertion 0top
|- ( J e. Top -> ( U. J = (/) <-> J = { (/) } ) )

Proof

Step Hyp Ref Expression
1 olc
 |-  ( J = { (/) } -> ( J = (/) \/ J = { (/) } ) )
2 0opn
 |-  ( J e. Top -> (/) e. J )
3 n0i
 |-  ( (/) e. J -> -. J = (/) )
4 2 3 syl
 |-  ( J e. Top -> -. J = (/) )
5 4 pm2.21d
 |-  ( J e. Top -> ( J = (/) -> J = { (/) } ) )
6 idd
 |-  ( J e. Top -> ( J = { (/) } -> J = { (/) } ) )
7 5 6 jaod
 |-  ( J e. Top -> ( ( J = (/) \/ J = { (/) } ) -> J = { (/) } ) )
8 1 7 impbid2
 |-  ( J e. Top -> ( J = { (/) } <-> ( J = (/) \/ J = { (/) } ) ) )
9 uni0b
 |-  ( U. J = (/) <-> J C_ { (/) } )
10 sssn
 |-  ( J C_ { (/) } <-> ( J = (/) \/ J = { (/) } ) )
11 9 10 bitr2i
 |-  ( ( J = (/) \/ J = { (/) } ) <-> U. J = (/) )
12 8 11 bitr2di
 |-  ( J e. Top -> ( U. J = (/) <-> J = { (/) } ) )