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 | ⊢ ω ≈ ( ω ∖ { ∅ } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omex | ⊢ ω ∈ V | |
2 | limom | ⊢ Lim ω | |
3 | 2 | limenpsi | ⊢ ( ω ∈ V → ω ≈ ( ω ∖ { ∅ } ) ) |
4 | 1 3 | ax-mp | ⊢ ω ≈ ( ω ∖ { ∅ } ) |