Metamath Proof Explorer


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 ω ≈ ( ω ∖ { ∅ } )