Description: Corollary of the Pigeonhole Principle php : a natural number is not equinumerous to its successor. Corollary 10.21(1) of TakeutiZaring p. 90. (Contributed by NM, 26-Jul-2004)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | php5 | |- ( A e. _om -> -. A ~~ suc A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | php4 | |- ( A e. _om -> A ~< suc A ) |
|
| 2 | sdomnen | |- ( A ~< suc A -> -. A ~~ suc A ) |
|
| 3 | 1 2 | syl | |- ( A e. _om -> -. A ~~ suc A ) |