This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )