This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ω ≈ ω ∖ ∅