Theorem oldfi

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

	Ref	Expression
Assertion	oldfi	|- ( A e. _om -> ( _Old ` A ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		oldval	|- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) )
3	1 2	syl	|- ( A e. _om -> ( _Old ` A ) = U. ( _Made " A ) )
4		madef	|- _Made : On --> ~P No
5		ffun	|- ( _Made : On --> ~P No -> Fun _Made )
6	4 5	ax-mp	|- Fun _Made
7		nnfi	|- ( A e. _om -> A e. Fin )
8		imafi	|- ( ( Fun _Made /\ A e. Fin ) -> ( _Made " A ) e. Fin )
9	6 7 8	sylancr	|- ( A e. _om -> ( _Made " A ) e. Fin )
10		elnn	|- ( ( x e. A /\ A e. _om ) -> x e. _om )
11	10	ancoms	|- ( ( A e. _om /\ x e. A ) -> x e. _om )
12		madefi	|- ( x e. _om -> ( _Made ` x ) e. Fin )
13	11 12	syl	|- ( ( A e. _om /\ x e. A ) -> ( _Made ` x ) e. Fin )
14	13	ralrimiva	|- ( A e. _om -> A. x e. A ( _Made ` x ) e. Fin )
15		onss	|- ( A e. On -> A C_ On )
16	1 15	syl	|- ( A e. _om -> A C_ On )
17	4	fdmi	|- dom _Made = On
18	16 17	sseqtrrdi	|- ( A e. _om -> A C_ dom _Made )
19		funimass4	|- ( ( Fun _Made /\ A C_ dom _Made ) -> ( ( _Made " A ) C_ Fin <-> A. x e. A ( _Made ` x ) e. Fin ) )
20	6 18 19	sylancr	|- ( A e. _om -> ( ( _Made " A ) C_ Fin <-> A. x e. A ( _Made ` x ) e. Fin ) )
21	14 20	mpbird	|- ( A e. _om -> ( _Made " A ) C_ Fin )
22		unifi	|- ( ( ( _Made " A ) e. Fin /\ ( _Made " A ) C_ Fin ) -> U. ( _Made " A ) e. Fin )
23	9 21 22	syl2anc	|- ( A e. _om -> U. ( _Made " A ) e. Fin )
24	3 23	eqeltrd	|- ( A e. _om -> ( _Old ` A ) e. Fin )