oldfi

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

		Ref	Expression
	Assertion	oldfi	$⊢ A \in ω \to Old (A) \in Fin$

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		oldval	$⊢ A \in On \to Old (A) = ⋃ M [A]$
3	1 2	syl	$⊢ A \in ω \to Old (A) = ⋃ M [A]$
4		madef	$⊢ M : On ⟶ 𝒫 No$
5		ffun	$⊢ M : On ⟶ 𝒫 No \to Fun M$
6	4 5	ax-mp	$⊢ Fun M$
7		nnfi	$⊢ A \in ω \to A \in Fin$
8		imafi	$⊢ (Fun M \land A \in Fin) \to M [A] \in Fin$
9	6 7 8	sylancr	$⊢ A \in ω \to M [A] \in Fin$
10		elnn	$⊢ (x \in A \land A \in ω) \to x \in ω$
11	10	ancoms	$⊢ (A \in ω \land x \in A) \to x \in ω$
12		madefi	$⊢ x \in ω \to M (x) \in Fin$
13	11 12	syl	$⊢ (A \in ω \land x \in A) \to M (x) \in Fin$
14	13	ralrimiva	$⊢ A \in ω \to \forall x \in A M (x) \in Fin$
15		onss	$⊢ A \in On \to A \subseteq On$
16	1 15	syl	$⊢ A \in ω \to A \subseteq On$
17	4	fdmi	$⊢ dom M = On$
18	16 17	sseqtrrdi	$⊢ A \in ω \to A \subseteq dom M$
19		funimass4	$⊢ (Fun M \land A \subseteq dom M) \to (M [A] \subseteq Fin \leftrightarrow \forall x \in A M (x) \in Fin)$
20	6 18 19	sylancr	$⊢ A \in ω \to (M [A] \subseteq Fin \leftrightarrow \forall x \in A M (x) \in Fin)$
21	14 20	mpbird	$⊢ A \in ω \to M [A] \subseteq Fin$
22		unifi	$⊢ (M [A] \in Fin \land M [A] \subseteq Fin) \to ⋃ M [A] \in Fin$
23	9 21 22	syl2anc	$⊢ A \in ω \to ⋃ M [A] \in Fin$
24	3 23	eqeltrd	$⊢ A \in ω \to Old (A) \in Fin$

Metamath Proof Explorer