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 e. _om -> A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		enrefnn	|- ( A e. _om -> A ~~ A )
2		breq2	|- ( x = A -> ( A ~~ x <-> A ~~ A ) )
3	2	rspcev	|- ( ( A e. _om /\ A ~~ A ) -> E. x e. _om A ~~ x )
4	1 3	mpdan	|- ( A e. _om -> E. x e. _om A ~~ x )
5		isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )
6	4 5	sylibr	|- ( A e. _om -> A e. Fin )