Theorem kardnnfi

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

	Ref	Expression
Assertion	kardnnfi	⊢ ( 𝐴 ∈ ω → ( kard ‘ 𝐴 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		onrankid	⊢ ( 𝐴 ∈ On ↔ ( rank ‘ 𝐴 ) = 𝐴 )
3	1 2	sylib	⊢ ( 𝐴 ∈ ω → ( rank ‘ 𝐴 ) = 𝐴 )
4	3	eleq1d	⊢ ( 𝐴 ∈ ω → ( ( rank ‘ 𝐴 ) ∈ ω ↔ 𝐴 ∈ ω ) )
5	4	ibir	⊢ ( 𝐴 ∈ ω → ( rank ‘ 𝐴 ) ∈ ω )
6		peano2	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → suc ( rank ‘ 𝐴 ) ∈ ω )
7		r1fin	⊢ ( suc ( rank ‘ 𝐴 ) ∈ ω → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∈ Fin )
8	5 6 7	3syl	⊢ ( 𝐴 ∈ ω → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∈ Fin )
9		kardval	⊢ ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 }
10		enrefnn	⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 )
11		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝐴 ↔ 𝐴 ≈ 𝐴 ) )
12	11	elabg	⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐴 } ↔ 𝐴 ≈ 𝐴 ) )
13	10 12	mpbird	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐴 } )
14		scottssr1	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐴 } → Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
15	13 14	syl	⊢ ( 𝐴 ∈ ω → Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
16	9 15	eqsstrid	⊢ ( 𝐴 ∈ ω → ( kard ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
17	8 16	ssfid	⊢ ( 𝐴 ∈ ω → ( kard ‘ 𝐴 ) ∈ Fin )