Description: Numeration theorem: any set is equinumerous to some ordinal (using AC). Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 20-Oct-2003)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | numth.1 | |- A e. _V |
|
| Assertion | numth2 | |- E. x e. On x ~~ A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | numth.1 | |- A e. _V |
|
| 2 | numth3 | |- ( A e. _V -> A e. dom card ) |
|
| 3 | 1 2 | ax-mp | |- A e. dom card |
| 4 | isnum2 | |- ( A e. dom card <-> E. x e. On x ~~ A ) |
|
| 5 | 3 4 | mpbi | |- E. x e. On x ~~ A |