Metamath Proof Explorer


Theorem isfiniteg

Description: A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of Suppes p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion isfiniteg
|- ( _om e. _V -> ( A e. Fin <-> A ~< _om ) )

Proof

Step Hyp Ref Expression
1 isfi
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
2 nnsdomg
 |-  ( ( _om e. _V /\ x e. _om ) -> x ~< _om )
3 sdomen1
 |-  ( A ~~ x -> ( A ~< _om <-> x ~< _om ) )
4 2 3 syl5ibrcom
 |-  ( ( _om e. _V /\ x e. _om ) -> ( A ~~ x -> A ~< _om ) )
5 4 rexlimdva
 |-  ( _om e. _V -> ( E. x e. _om A ~~ x -> A ~< _om ) )
6 1 5 syl5bi
 |-  ( _om e. _V -> ( A e. Fin -> A ~< _om ) )
7 isfinite2
 |-  ( A ~< _om -> A e. Fin )
8 6 7 impbid1
 |-  ( _om e. _V -> ( A e. Fin <-> A ~< _om ) )