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 JTopJ=J=

Proof

Step Hyp Ref Expression
1 olc J=J=J=
2 0opn JTopJ
3 n0i J¬J=
4 2 3 syl JTop¬J=
5 4 pm2.21d JTopJ=J=
6 idd JTopJ=J=
7 5 6 jaod JTopJ=J=J=
8 1 7 impbid2 JTopJ=J=J=
9 uni0b J=J
10 sssn JJ=J=
11 9 10 bitr2i J=J=J=
12 8 11 bitr2di JTopJ=J=