Metamath Proof Explorer


Theorem fict

Description: A finite set is countable (weaker version of isfinite ). (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Assertion fict
|- ( A e. Fin -> A ~<_ _om )

Proof

Step Hyp Ref Expression
1 isfinite
 |-  ( A e. Fin <-> A ~< _om )
2 sdomdom
 |-  ( A ~< _om -> A ~<_ _om )
3 1 2 sylbi
 |-  ( A e. Fin -> A ~<_ _om )