This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Fin \to A ≼ ω$

Step	Hyp	Ref	Expression
1		isfinite	$⊢ A \in Fin \leftrightarrow A ≺ ω$
2		sdomdom	$⊢ A ≺ ω \to A ≼ ω$
3	1 2	sylbi	$⊢ A \in Fin \to A ≼ ω$