Metamath Proof Explorer

Theorem 0fin

Description: The empty set is finite. (Contributed by FL, 14-Jul-2008)

Ref Expression
Assertion 0fin 
|- (/) e. Fin

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 ssid 
 |-  (/) C_ (/)
3 ssnnfi 
 |-  ( ( (/) e. _om /\ (/) C_ (/) ) -> (/) e. Fin )
4 1 2 3 mp2an 
 |-  (/) e. Fin