Theorem omenps

Description: Omega is equinumerous to a proper subset of itself. Example 13.2(4) of Eisenberg p. 216. (Contributed by NM, 30-Jul-2003)

	Ref	Expression
Assertion	omenps	⊢ ω ≈ ( ω ∖ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		limom	⊢ Lim ω
3	2	limenpsi	⊢ ( ω ∈ V → ω ≈ ( ω ∖ { ∅ } ) )
4	1 3	ax-mp	⊢ ω ≈ ( ω ∖ { ∅ } )