Theorem kardnnfi

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

	Ref	Expression
Assertion	kardnnfi	Could not format assertion : No typesetting found for |- ( A e. _om -> ( kard ` A ) e. Fin ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nnon	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{On}$$
2		onrankid	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{rank}\left(A\right)=A$$
3	1 2	sylib	$$⊢A\in \mathrm{\omega }\to \mathrm{rank}\left(A\right)=A$$
4	3	eleq1d	$$⊢A\in \mathrm{\omega }\to \left(\mathrm{rank}\left(A\right)\in \mathrm{\omega }\leftrightarrow A\in \mathrm{\omega }\right)$$
5	4	ibir	$$⊢A\in \mathrm{\omega }\to \mathrm{rank}\left(A\right)\in \mathrm{\omega }$$
6		peano2	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{\omega }\to \mathrm{suc}\mathrm{rank}\left(A\right)\in \mathrm{\omega }$$
7		r1fin	$$⊢\mathrm{suc}\mathrm{rank}\left(A\right)\in \mathrm{\omega }\to R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)\in \mathrm{Fin}$$
8	5 6 7	3syl	$$⊢A\in \mathrm{\omega }\to R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)\in \mathrm{Fin}$$
9		kardval	Could not format ( kard ` A ) = Scott { x | x ~~ A } : No typesetting found for |- ( kard ` A ) = Scott { x | x ~~ A } with typecode |-
10		enrefnn	$$⊢A\in \mathrm{\omega }\to A\approx A$$
11		breq1	$$⊢x=A\to \left(x\approx A\leftrightarrow A\approx A\right)$$
12	11	elabg	$$⊢A\in \mathrm{\omega }\to \left(A\in \left\{x|x\approx A\right\}\leftrightarrow A\approx A\right)$$
13	10 12	mpbird	$$⊢A\in \mathrm{\omega }\to A\in \left\{x|x\approx A\right\}$$
14		scottssr1	$$⊢A\in \left\{x|x\approx A\right\}\to Scott\left\{x|x\approx A\right\}\subseteq R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)$$
15	13 14	syl	$$⊢A\in \mathrm{\omega }\to Scott\left\{x|x\approx A\right\}\subseteq R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)$$
16	9 15	eqsstrid	Could not format ( A e. _om -> ( kard ` A ) C_ ( R1 ` suc ( rank ` A ) ) ) : No typesetting found for |- ( A e. _om -> ( kard ` A ) C_ ( R1 ` suc ( rank ` A ) ) ) with typecode |-
17	8 16	ssfid	Could not format ( A e. _om -> ( kard ` A ) e. Fin ) : No typesetting found for |- ( A e. _om -> ( kard ` A ) e. Fin ) with typecode |-