Theorem kardnnfi

Description: The kard cardinal number of a finite ordinal is finite. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardnnfi	|- ( A e. _om -> ( kard ` A ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		onrankid	|- ( A e. On <-> ( rank ` A ) = A )
3	1 2	sylib	|- ( A e. _om -> ( rank ` A ) = A )
4	3	eleq1d	|- ( A e. _om -> ( ( rank ` A ) e. _om <-> A e. _om ) )
5	4	ibir	|- ( A e. _om -> ( rank ` A ) e. _om )
6		peano2	|- ( ( rank ` A ) e. _om -> suc ( rank ` A ) e. _om )
7		r1fin	|- ( suc ( rank ` A ) e. _om -> ( R1 ` suc ( rank ` A ) ) e. Fin )
8	5 6 7	3syl	|- ( A e. _om -> ( R1 ` suc ( rank ` A ) ) e. Fin )
9		kardval	|- ( kard ` A ) = Scott { x | x ~~ A }
10		enrefnn	|- ( A e. _om -> A ~~ A )
11		breq1	|- ( x = A -> ( x ~~ A <-> A ~~ A ) )
12	11	elabg	|- ( A e. _om -> ( A e. { x | x ~~ A } <-> A ~~ A ) )
13	10 12	mpbird	|- ( A e. _om -> A e. { x | x ~~ A } )
14		scottssr1	|- ( A e. { x | x ~~ A } -> Scott { x | x ~~ A } C_ ( R1 ` suc ( rank ` A ) ) )
15	13 14	syl	|- ( A e. _om -> Scott { x | x ~~ A } C_ ( R1 ` suc ( rank ` A ) ) )
16	9 15	eqsstrid	|- ( A e. _om -> ( kard ` A ) C_ ( R1 ` suc ( rank ` A ) ) )
17	8 16	ssfid	|- ( A e. _om -> ( kard ` A ) e. Fin )