Metamath Proof Explorer


Theorem isfinite

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 Fin A ω

Proof

Step Hyp Ref Expression
1 omex ω V
2 isfiniteg ω V A Fin A ω
3 1 2 ax-mp A Fin A ω