Theorem omensuc

Description: The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003)

	Ref	Expression
Assertion	omensuc	⊢ ω ≈ suc ω

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		limom	⊢ Lim ω
3	2	limensuci	⊢ ( ω ∈ V → ω ≈ suc ω )
4	1 3	ax-mp	⊢ ω ≈ suc ω