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 )