Theorem oldfi

Description: The old set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Assertion	oldfi	⊢ ( 𝐴 ∈ ω → ( O ‘ 𝐴 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		oldval	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ω → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
4		madef	⊢ M : On ⟶ 𝒫 No
5		ffun	⊢ ( M : On ⟶ 𝒫 No → Fun M )
6	4 5	ax-mp	⊢ Fun M
7		nnfi	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
8		imafi	⊢ ( ( Fun M ∧ 𝐴 ∈ Fin ) → ( M “ 𝐴 ) ∈ Fin )
9	6 7 8	sylancr	⊢ ( 𝐴 ∈ ω → ( M “ 𝐴 ) ∈ Fin )
10		elnn	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ω ) → 𝑥 ∈ ω )
11	10	ancoms	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ω )
12		madefi	⊢ ( 𝑥 ∈ ω → ( M ‘ 𝑥 ) ∈ Fin )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ 𝐴 ) → ( M ‘ 𝑥 ) ∈ Fin )
14	13	ralrimiva	⊢ ( 𝐴 ∈ ω → ∀ 𝑥 ∈ 𝐴 ( M ‘ 𝑥 ) ∈ Fin )
15		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
16	1 15	syl	⊢ ( 𝐴 ∈ ω → 𝐴 ⊆ On )
17	4	fdmi	⊢ dom M = On
18	16 17	sseqtrrdi	⊢ ( 𝐴 ∈ ω → 𝐴 ⊆ dom M )
19		funimass4	⊢ ( ( Fun M ∧ 𝐴 ⊆ dom M ) → ( ( M “ 𝐴 ) ⊆ Fin ↔ ∀ 𝑥 ∈ 𝐴 ( M ‘ 𝑥 ) ∈ Fin ) )
20	6 18 19	sylancr	⊢ ( 𝐴 ∈ ω → ( ( M “ 𝐴 ) ⊆ Fin ↔ ∀ 𝑥 ∈ 𝐴 ( M ‘ 𝑥 ) ∈ Fin ) )
21	14 20	mpbird	⊢ ( 𝐴 ∈ ω → ( M “ 𝐴 ) ⊆ Fin )
22		unifi	⊢ ( ( ( M “ 𝐴 ) ∈ Fin ∧ ( M “ 𝐴 ) ⊆ Fin ) → ∪ ( M “ 𝐴 ) ∈ Fin )
23	9 21 22	syl2anc	⊢ ( 𝐴 ∈ ω → ∪ ( M “ 𝐴 ) ∈ Fin )
24	3 23	eqeltrd	⊢ ( 𝐴 ∈ ω → ( O ‘ 𝐴 ) ∈ Fin )