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