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	|- _om = ( On i^i Fin )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( x e. _om -> x e. On )
2		onfin	|- ( x e. On -> ( x e. Fin <-> x e. _om ) )
3	2	biimprcd	|- ( x e. _om -> ( x e. On -> x e. Fin ) )
4	1 3	jcai	|- ( x e. _om -> ( x e. On /\ x e. Fin ) )
5	2	biimpa	|- ( ( x e. On /\ x e. Fin ) -> x e. _om )
6	4 5	impbii	|- ( x e. _om <-> ( x e. On /\ x e. Fin ) )
7		elin	|- ( x e. ( On i^i Fin ) <-> ( x e. On /\ x e. Fin ) )
8	6 7	bitr4i	|- ( x e. _om <-> x e. ( On i^i Fin ) )
9	8	eqriv	|- _om = ( On i^i Fin )