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 
|- _om ~~ ( _om \ { (/) } )

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 limom 
 |-  Lim _om
3 2 limenpsi 
 |-  ( _om e. _V -> _om ~~ ( _om \ { (/) } ) )
4 1 3 ax-mp 
 |-  _om ~~ ( _om \ { (/) } )