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 ωω