This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0cmp

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

		Ref	Expression
	Assertion	0cmp	$⊢ \{\emptyset\} \in Comp$

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