Description: The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf . (Contributed by NM, 7-Nov-2008)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cardsucnn | |- ( A e. _om -> ( card ` suc A ) = suc ( card ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano2 | |- ( A e. _om -> suc A e. _om ) |
|
| 2 | cardnn | |- ( suc A e. _om -> ( card ` suc A ) = suc A ) |
|
| 3 | 1 2 | syl | |- ( A e. _om -> ( card ` suc A ) = suc A ) |
| 4 | cardnn | |- ( A e. _om -> ( card ` A ) = A ) |
|
| 5 | suceq | |- ( ( card ` A ) = A -> suc ( card ` A ) = suc A ) |
|
| 6 | 4 5 | syl | |- ( A e. _om -> suc ( card ` A ) = suc A ) |
| 7 | 3 6 | eqtr4d | |- ( A e. _om -> ( card ` suc A ) = suc ( card ` A ) ) |