Theorem onfin

Description: An ordinal number is finite iff it is a natural number. Proposition 10.32 of TakeutiZaring p. 92. (Contributed by NM, 26-Jul-2004)

	Ref	Expression
Assertion	onfin	|- ( A e. On -> ( A e. Fin <-> A e. _om ) )

Proof

Step	Hyp	Ref	Expression
1		isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )
2		onomeneq	|- ( ( A e. On /\ x e. _om ) -> ( A ~~ x <-> A = x ) )
3		eleq1a	|- ( x e. _om -> ( A = x -> A e. _om ) )
4	3	adantl	|- ( ( A e. On /\ x e. _om ) -> ( A = x -> A e. _om ) )
5	2 4	sylbid	|- ( ( A e. On /\ x e. _om ) -> ( A ~~ x -> A e. _om ) )
6	5	rexlimdva	|- ( A e. On -> ( E. x e. _om A ~~ x -> A e. _om ) )
7		enrefnn	|- ( A e. _om -> A ~~ A )
8		breq2	|- ( x = A -> ( A ~~ x <-> A ~~ A ) )
9	8	rspcev	|- ( ( A e. _om /\ A ~~ A ) -> E. x e. _om A ~~ x )
10	7 9	mpdan	|- ( A e. _om -> E. x e. _om A ~~ x )
11	6 10	impbid1	|- ( A e. On -> ( E. x e. _om A ~~ x <-> A e. _om ) )
12	1 11	bitrid	|- ( A e. On -> ( A e. Fin <-> A e. _om ) )