Theorem nnfi

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015) Avoid ax-pow . (Revised by BTernaryTau, 23-Sep-2024)

	Ref	Expression
Assertion	nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		enrefnn	$$⊢A\in \mathrm{\omega }\to A\approx A$$
2		breq2	$$⊢x=A\to \left(A\approx x\leftrightarrow A\approx A\right)$$
3	2	rspcev	$$⊢\left(A\in \mathrm{\omega }\wedge A\approx A\right)\to \exists x\in \mathrm{\omega }A\approx x$$
4	1 3	mpdan	$$⊢A\in \mathrm{\omega }\to \exists x\in \mathrm{\omega }A\approx x$$
5		isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
6	4 5	sylibr	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$