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 )