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\in \mathrm{Top}\to \left(\bigcup J=\varnothing \leftrightarrow J=\left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		olc	$$⊢J=\left\{\varnothing \right\}\to \left(J=\varnothing \vee J=\left\{\varnothing \right\}\right)$$
2		0opn	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$
3		n0i	$$⊢\varnothing \in J\to \neg J=\varnothing$$
4	2 3	syl	$$⊢J\in \mathrm{Top}\to \neg J=\varnothing$$
5	4	pm2.21d	$$⊢J\in \mathrm{Top}\to \left(J=\varnothing \to J=\left\{\varnothing \right\}\right)$$
6		idd	$$⊢J\in \mathrm{Top}\to \left(J=\left\{\varnothing \right\}\to J=\left\{\varnothing \right\}\right)$$
7	5 6	jaod	$$⊢J\in \mathrm{Top}\to \left(\left(J=\varnothing \vee J=\left\{\varnothing \right\}\right)\to J=\left\{\varnothing \right\}\right)$$
8	1 7	impbid2	$$⊢J\in \mathrm{Top}\to \left(J=\left\{\varnothing \right\}\leftrightarrow \left(J=\varnothing \vee J=\left\{\varnothing \right\}\right)\right)$$
9		uni0b	$$⊢\bigcup J=\varnothing \leftrightarrow J\subseteq \left\{\varnothing \right\}$$
10		sssn	$$⊢J\subseteq \left\{\varnothing \right\}\leftrightarrow \left(J=\varnothing \vee J=\left\{\varnothing \right\}\right)$$
11	9 10	bitr2i	$$⊢\left(J=\varnothing \vee J=\left\{\varnothing \right\}\right)\leftrightarrow \bigcup J=\varnothing$$
12	8 11	bitr2di	$$⊢J\in \mathrm{Top}\to \left(\bigcup J=\varnothing \leftrightarrow J=\left\{\varnothing \right\}\right)$$