Description: A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of Suppes p. 151. The Axiom of Infinity is used for the forward implication. (Contributed by FL, 16-Apr-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isfinite | |- ( A e. Fin <-> A ~< _om ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omex | |- _om e. _V |
|
| 2 | isfiniteg | |- ( _om e. _V -> ( A e. Fin <-> A ~< _om ) ) |
|
| 3 | 1 2 | ax-mp | |- ( A e. Fin <-> A ~< _om ) |