Theorem finnum

Description: Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	finnum	$$⊢A\in \mathrm{Fin}\to A\in \mathrm{dom}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
2		nnon	$$⊢x\in \mathrm{\omega }\to x\in \mathrm{On}$$
3		ensym	$$⊢A\approx x\to x\approx A$$
4		isnumi	$$⊢\left(x\in \mathrm{On}\wedge x\approx A\right)\to A\in \mathrm{dom}\mathrm{card}$$
5	2 3 4	syl2an	$$⊢\left(x\in \mathrm{\omega }\wedge A\approx x\right)\to A\in \mathrm{dom}\mathrm{card}$$
6	5	rexlimiva	$$⊢\exists x\in \mathrm{\omega }A\approx x\to A\in \mathrm{dom}\mathrm{card}$$
7	1 6	sylbi	$$⊢A\in \mathrm{Fin}\to A\in \mathrm{dom}\mathrm{card}$$