Theorem fisdomnn

Description: A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025)

	Ref	Expression
Assertion	fisdomnn	$$⊢A\in \mathrm{Fin}\to A\prec \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		canth2g	$$⊢A\in \mathrm{Fin}\to A\prec 𝒫A$$
2		pwfi	$$⊢A\in \mathrm{Fin}\leftrightarrow 𝒫A\in \mathrm{Fin}$$
3		fzfi	$$⊢\left(1\dots \left|𝒫A\right|\right)\in \mathrm{Fin}$$
4		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
5		fz1ssnn	$$⊢\left(1\dots \left|𝒫A\right|\right)\subseteq \mathbb{N}$$
6		ssdomfi2	$$⊢\left(\left(1\dots \left|𝒫A\right|\right)\in \mathrm{Fin}\wedge \mathbb{N}\in \mathrm{V}\wedge \left(1\dots \left|𝒫A\right|\right)\subseteq \mathbb{N}\right)\to \left(1\dots \left|𝒫A\right|\right)\preccurlyeq \mathbb{N}$$
7	3 4 5 6	mp3an	$$⊢\left(1\dots \left|𝒫A\right|\right)\preccurlyeq \mathbb{N}$$
8		isfinite4	$$⊢𝒫A\in \mathrm{Fin}\leftrightarrow \left(1\dots \left|𝒫A\right|\right)\approx 𝒫A$$
9		domen1	$$⊢\left(1\dots \left|𝒫A\right|\right)\approx 𝒫A\to \left(\left(1\dots \left|𝒫A\right|\right)\preccurlyeq \mathbb{N}\leftrightarrow 𝒫A\preccurlyeq \mathbb{N}\right)$$
10	8 9	sylbi	$$⊢𝒫A\in \mathrm{Fin}\to \left(\left(1\dots \left|𝒫A\right|\right)\preccurlyeq \mathbb{N}\leftrightarrow 𝒫A\preccurlyeq \mathbb{N}\right)$$
11	7 10	mpbii	$$⊢𝒫A\in \mathrm{Fin}\to 𝒫A\preccurlyeq \mathbb{N}$$
12	2 11	sylbi	$$⊢A\in \mathrm{Fin}\to 𝒫A\preccurlyeq \mathbb{N}$$
13		sdomdomtrfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\prec 𝒫A\wedge 𝒫A\preccurlyeq \mathbb{N}\right)\to A\prec \mathbb{N}$$
14	1 12 13	mpd3an23	$$⊢A\in \mathrm{Fin}\to A\prec \mathbb{N}$$