Theorem unbnn3

Description: Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005)

	Ref	Expression
Assertion	unbnn3	|- ( ( A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A ~~ _om )

Proof

Step	Hyp	Ref	Expression
1		omex	|- _om e. _V
2		unbnn	|- ( ( _om e. _V /\ A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A ~~ _om )
3	1 2	mp3an1	|- ( ( A C_ _om /\ A. x e. _om E. y e. A x e. y ) -> A ~~ _om )