Theorem fmtnoinf

Description: The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021)

	Ref	Expression
Assertion	fmtnoinf	$$⊢\mathrm{ran}\mathrm{FermatNo}\notin \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fmtnof1	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}$$
2		f1f	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}\to \mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}$$
3		fdm	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}\to \mathrm{dom}\mathrm{FermatNo}={\mathbb{N}}_0$$
4		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
5		nnnfi	$$⊢\neg \mathbb{N}\in \mathrm{Fin}$$
6		ssfi	$$⊢\left({\mathbb{N}}_0\in \mathrm{Fin}\wedge \mathbb{N}\subseteq {\mathbb{N}}_0\right)\to \mathbb{N}\in \mathrm{Fin}$$
7	6	expcom	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left({\mathbb{N}}_0\in \mathrm{Fin}\to \mathbb{N}\in \mathrm{Fin}\right)$$
8	7	con3d	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left(\neg \mathbb{N}\in \mathrm{Fin}\to \neg {\mathbb{N}}_0\in \mathrm{Fin}\right)$$
9	4 5 8	mp2	$$⊢\neg {\mathbb{N}}_0\in \mathrm{Fin}$$
10		eleq1	$$⊢\mathrm{dom}\mathrm{FermatNo}={\mathbb{N}}_0\to \left(\mathrm{dom}\mathrm{FermatNo}\in \mathrm{Fin}\leftrightarrow {\mathbb{N}}_0\in \mathrm{Fin}\right)$$
11	9 10	mtbiri	$$⊢\mathrm{dom}\mathrm{FermatNo}={\mathbb{N}}_0\to \neg \mathrm{dom}\mathrm{FermatNo}\in \mathrm{Fin}$$
12	3 11	syl	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}\to \neg \mathrm{dom}\mathrm{FermatNo}\in \mathrm{Fin}$$
13		ffun	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}\to \mathrm{Fun}\mathrm{FermatNo}$$
14		fundmfibi	$$⊢\mathrm{Fun}\mathrm{FermatNo}\to \left(\mathrm{FermatNo}\in \mathrm{Fin}\leftrightarrow \mathrm{dom}\mathrm{FermatNo}\in \mathrm{Fin}\right)$$
15	13 14	syl	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}\to \left(\mathrm{FermatNo}\in \mathrm{Fin}\leftrightarrow \mathrm{dom}\mathrm{FermatNo}\in \mathrm{Fin}\right)$$
16	12 15	mtbird	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}\to \neg \mathrm{FermatNo}\in \mathrm{Fin}$$
17	1 2 16	mp2b	$$⊢\neg \mathrm{FermatNo}\in \mathrm{Fin}$$
18		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
19		f1dmvrnfibi	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}\right)\to \left(\mathrm{FermatNo}\in \mathrm{Fin}\leftrightarrow \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}\right)$$
20	19	notbid	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge \mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}\right)\to \left(\neg \mathrm{FermatNo}\in \mathrm{Fin}\leftrightarrow \neg \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}\right)$$
21	18 1 20	mp2an	$$⊢\neg \mathrm{FermatNo}\in \mathrm{Fin}\leftrightarrow \neg \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}$$
22	17 21	mpbi	$$⊢\neg \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}$$
23	22	nelir	$$⊢\mathrm{ran}\mathrm{FermatNo}\notin \mathrm{Fin}$$