Theorem 0cmp

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

	Ref	Expression
Assertion	0cmp	⊢ { ∅ } ∈ Comp

Proof

Step	Hyp	Ref	Expression
1		sn0top	⊢ { ∅ } ∈ Top
2		snfi	⊢ { ∅ } ∈ Fin
3	1 2	elini	⊢ { ∅ } ∈ ( Top ∩ Fin )
4		fincmp	⊢ ( { ∅ } ∈ ( Top ∩ Fin ) → { ∅ } ∈ Comp )
5	3 4	ax-mp	⊢ { ∅ } ∈ Comp