Metamath Proof Explorer

Theorem finnum

Description: Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion finnum 
|- ( A e. Fin -> A e. dom card )

Proof

Step Hyp Ref Expression
1 isfi 
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
2 nnon 
 |-  ( x e. _om -> x e. On )
3 ensym 
 |-  ( A ~~ x -> x ~~ A )
4 isnumi 
 |-  ( ( x e. On /\ x ~~ A ) -> A e. dom card )
5 2 3 4 syl2an 
 |-  ( ( x e. _om /\ A ~~ x ) -> A e. dom card )
6 5 rexlimiva 
 |-  ( E. x e. _om A ~~ x -> A e. dom card )
7 1 6 sylbi 
 |-  ( A e. Fin -> A e. dom card )