Metamath Proof Explorer


Theorem 0fin

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

Ref Expression
Assertion 0fin Fin

Proof

Step Hyp Ref Expression
1 peano1 ω
2 ssid
3 ssnnfi ω Fin
4 1 2 3 mp2an Fin