Theorem 0cmp

Description: The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009)

	Ref	Expression
Assertion	0cmp	$$⊢\left\{\varnothing \right\}\in \mathrm{Comp}$$

Proof

Step	Hyp	Ref	Expression
1		sn0top	$$⊢\left\{\varnothing \right\}\in \mathrm{Top}$$
2		snfi	$$⊢\left\{\varnothing \right\}\in \mathrm{Fin}$$
3	1 2	elini	$$⊢\left\{\varnothing \right\}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)$$
4		fincmp	$$⊢\left\{\varnothing \right\}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to \left\{\varnothing \right\}\in \mathrm{Comp}$$
5	3 4	ax-mp	$$⊢\left\{\varnothing \right\}\in \mathrm{Comp}$$