Metamath Proof Explorer

Theorem 0cmp

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

Ref Expression
Assertion 0cmp 
|- { (/) } e. Comp

Proof

Step Hyp Ref Expression
1 sn0top 
 |-  { (/) } e. Top
2 snfi 
 |-  { (/) } e. Fin
3 1 2 elini 
 |-  { (/) } e. ( Top i^i Fin )
4 fincmp 
 |-  ( { (/) } e. ( Top i^i Fin ) -> { (/) } e. Comp )
5 3 4 ax-mp 
 |-  { (/) } e. Comp