# Metamath Proof Explorer

## Theorem onfin2

Description: A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013)

Ref Expression
Assertion onfin2 ${⊢}\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 nnon ${⊢}{x}\in \mathrm{\omega }\to {x}\in \mathrm{On}$
2 onfin ${⊢}{x}\in \mathrm{On}\to \left({x}\in \mathrm{Fin}↔{x}\in \mathrm{\omega }\right)$
3 2 biimprcd ${⊢}{x}\in \mathrm{\omega }\to \left({x}\in \mathrm{On}\to {x}\in \mathrm{Fin}\right)$
4 1 3 jcai ${⊢}{x}\in \mathrm{\omega }\to \left({x}\in \mathrm{On}\wedge {x}\in \mathrm{Fin}\right)$
5 2 biimpa ${⊢}\left({x}\in \mathrm{On}\wedge {x}\in \mathrm{Fin}\right)\to {x}\in \mathrm{\omega }$
6 4 5 impbii ${⊢}{x}\in \mathrm{\omega }↔\left({x}\in \mathrm{On}\wedge {x}\in \mathrm{Fin}\right)$
7 elin ${⊢}{x}\in \left(\mathrm{On}\cap \mathrm{Fin}\right)↔\left({x}\in \mathrm{On}\wedge {x}\in \mathrm{Fin}\right)$
8 6 7 bitr4i ${⊢}{x}\in \mathrm{\omega }↔{x}\in \left(\mathrm{On}\cap \mathrm{Fin}\right)$
9 8 eqriv ${⊢}\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$