This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ficardom

Description: The cardinal number of a finite set is a finite ordinal. (Contributed by Paul Chapman, 11-Apr-2009) (Revised by Mario Carneiro, 4-Feb-2013)

Ref Expression
Assertion ficardom 
|- ( A e. Fin -> ( card ` A ) e. _om )

Proof

Step Hyp Ref Expression
1 isfi 
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
2 1 biimpi 
 |-  ( A e. Fin -> E. x e. _om A ~~ x )
3 finnum 
 |-  ( A e. Fin -> A e. dom card )
4 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
5 3 4 syl 
 |-  ( A e. Fin -> ( card ` A ) ~~ A )
6 entr 
 |-  ( ( ( card ` A ) ~~ A /\ A ~~ x ) -> ( card ` A ) ~~ x )
7 5 6 sylan 
 |-  ( ( A e. Fin /\ A ~~ x ) -> ( card ` A ) ~~ x )
8 cardon 
 |-  ( card ` A ) e. On
9 onomeneq 
 |-  ( ( ( card ` A ) e. On /\ x e. _om ) -> ( ( card ` A ) ~~ x <-> ( card ` A ) = x ) )
10 8 9 mpan 
 |-  ( x e. _om -> ( ( card ` A ) ~~ x <-> ( card ` A ) = x ) )
11 7 10 imbitrid 
 |-  ( x e. _om -> ( ( A e. Fin /\ A ~~ x ) -> ( card ` A ) = x ) )
12 eleq1a 
 |-  ( x e. _om -> ( ( card ` A ) = x -> ( card ` A ) e. _om ) )
13 11 12 syld 
 |-  ( x e. _om -> ( ( A e. Fin /\ A ~~ x ) -> ( card ` A ) e. _om ) )
14 13 expcomd 
 |-  ( x e. _om -> ( A ~~ x -> ( A e. Fin -> ( card ` A ) e. _om ) ) )
15 14 rexlimiv 
 |-  ( E. x e. _om A ~~ x -> ( A e. Fin -> ( card ` A ) e. _om ) )
16 2 15 mpcom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )