Theorem oldfib

Description: The old set of an ordinal is finite iff the ordinal is finite. (Contributed by Scott Fenton, 19-Feb-2026)

	Ref	Expression
Assertion	oldfib	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ ω ↔ ( O ‘ 𝐴 ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		oldfi	⊢ ( 𝐴 ∈ ω → ( O ‘ 𝐴 ) ∈ Fin )
2		fveq2	⊢ ( 𝑥 = 𝑦 → ( O ‘ 𝑥 ) = ( O ‘ 𝑦 ) )
3	2	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( O ‘ 𝑥 ) ∈ Fin ↔ ( O ‘ 𝑦 ) ∈ Fin ) )
4		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ω ↔ 𝑦 ∈ ω ) )
5	3 4	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( O ‘ 𝑥 ) ∈ Fin → 𝑥 ∈ ω ) ↔ ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ) )
6		fveq2	⊢ ( 𝑥 = 𝐴 → ( O ‘ 𝑥 ) = ( O ‘ 𝐴 ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( O ‘ 𝑥 ) ∈ Fin ↔ ( O ‘ 𝐴 ) ∈ Fin ) )
8		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ω ↔ 𝐴 ∈ ω ) )
9	7 8	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( O ‘ 𝑥 ) ∈ Fin → 𝑥 ∈ ω ) ↔ ( ( O ‘ 𝐴 ) ∈ Fin → 𝐴 ∈ ω ) ) )
10		oldval	⊢ ( 𝑥 ∈ On → ( O ‘ 𝑥 ) = ∪ ( M “ 𝑥 ) )
11	10	eleq1d	⊢ ( 𝑥 ∈ On → ( ( O ‘ 𝑥 ) ∈ Fin ↔ ∪ ( M “ 𝑥 ) ∈ Fin ) )
12	11	biimpa	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ∪ ( M “ 𝑥 ) ∈ Fin )
13		unifi3	⊢ ( ∪ ( M “ 𝑥 ) ∈ Fin → ( M “ 𝑥 ) ⊆ Fin )
14	12 13	syl	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( M “ 𝑥 ) ⊆ Fin )
15		madef	⊢ M : On ⟶ 𝒫 No
16		ffun	⊢ ( M : On ⟶ 𝒫 No → Fun M )
17	15 16	ax-mp	⊢ Fun M
18		onss	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
19	15	fdmi	⊢ dom M = On
20	18 19	sseqtrrdi	⊢ ( 𝑥 ∈ On → 𝑥 ⊆ dom M )
21		funimass4	⊢ ( ( Fun M ∧ 𝑥 ⊆ dom M ) → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
22	17 20 21	sylancr	⊢ ( 𝑥 ∈ On → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
23	22	adantr	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( ( M “ 𝑥 ) ⊆ Fin ↔ ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin ) )
24	14 23	mpbid	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin )
25		oldssmade	⊢ ( O ‘ 𝑦 ) ⊆ ( M ‘ 𝑦 )
26		ssfi	⊢ ( ( ( M ‘ 𝑦 ) ∈ Fin ∧ ( O ‘ 𝑦 ) ⊆ ( M ‘ 𝑦 ) ) → ( O ‘ 𝑦 ) ∈ Fin )
27	25 26	mpan2	⊢ ( ( M ‘ 𝑦 ) ∈ Fin → ( O ‘ 𝑦 ) ∈ Fin )
28	27	ralimi	⊢ ( ∀ 𝑦 ∈ 𝑥 ( M ‘ 𝑦 ) ∈ Fin → ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin )
29	24 28	syl	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin )
30	29	3adant2	⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin )
31		r19.26	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑦 ) ∈ Fin ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin ) )
32		pm2.27	⊢ ( ( O ‘ 𝑦 ) ∈ Fin → ( ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) → 𝑦 ∈ ω ) )
33	32	impcom	⊢ ( ( ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑦 ) ∈ Fin ) → 𝑦 ∈ ω )
34	33	ralimi	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑦 ) ∈ Fin ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ω )
35		dfss3	⊢ ( 𝑥 ⊆ ω ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ω )
36	34 35	sylibr	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑦 ) ∈ Fin ) → 𝑥 ⊆ ω )
37	31 36	sylbir	⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin ) → 𝑥 ⊆ ω )
38		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
39		ordom	⊢ Ord ω
40		ordsseleq	⊢ ( ( Ord 𝑥 ∧ Ord ω ) → ( 𝑥 ⊆ ω ↔ ( 𝑥 ∈ ω ∨ 𝑥 = ω ) ) )
41	39 40	mpan2	⊢ ( Ord 𝑥 → ( 𝑥 ⊆ ω ↔ ( 𝑥 ∈ ω ∨ 𝑥 = ω ) ) )
42	38 41	syl	⊢ ( 𝑥 ∈ On → ( 𝑥 ⊆ ω ↔ ( 𝑥 ∈ ω ∨ 𝑥 = ω ) ) )
43	42	adantr	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( 𝑥 ⊆ ω ↔ ( 𝑥 ∈ ω ∨ 𝑥 = ω ) ) )
44		fveq2	⊢ ( 𝑥 = ω → ( O ‘ 𝑥 ) = ( O ‘ ω ) )
45		eqvisset	⊢ ( 𝑥 = ω → ω ∈ V )
46		bdayfun	⊢ Fun bday
47		n0sexg	⊢ ( ω ∈ V → ℕ0s ∈ V )
48		resfunexg	⊢ ( ( Fun bday ∧ ℕ0s ∈ V ) → ( bday ↾ ℕ0s ) ∈ V )
49	46 47 48	sylancr	⊢ ( ω ∈ V → ( bday ↾ ℕ0s ) ∈ V )
50		cnvexg	⊢ ( ( bday ↾ ℕ0s ) ∈ V → ◡ ( bday ↾ ℕ0s ) ∈ V )
51	49 50	syl	⊢ ( ω ∈ V → ◡ ( bday ↾ ℕ0s ) ∈ V )
52		bdayn0sf1o	⊢ ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω
53	52	a1i	⊢ ( ω ∈ V → ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω )
54		f1ocnv	⊢ ( ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω → ◡ ( bday ↾ ℕ0s ) : ω –1-1-onto→ ℕ0s )
55		f1of1	⊢ ( ◡ ( bday ↾ ℕ0s ) : ω –1-1-onto→ ℕ0s → ◡ ( bday ↾ ℕ0s ) : ω –1-1→ ℕ0s )
56	53 54 55	3syl	⊢ ( ω ∈ V → ◡ ( bday ↾ ℕ0s ) : ω –1-1→ ℕ0s )
57		n0ssoldg	⊢ ( ω ∈ V → ℕ0s ⊆ ( O ‘ ω ) )
58		f1ss	⊢ ( ( ◡ ( bday ↾ ℕ0s ) : ω –1-1→ ℕ0s ∧ ℕ0s ⊆ ( O ‘ ω ) ) → ◡ ( bday ↾ ℕ0s ) : ω –1-1→ ( O ‘ ω ) )
59	56 57 58	syl2anc	⊢ ( ω ∈ V → ◡ ( bday ↾ ℕ0s ) : ω –1-1→ ( O ‘ ω ) )
60		f1eq1	⊢ ( 𝑓 = ◡ ( bday ↾ ℕ0s ) → ( 𝑓 : ω –1-1→ ( O ‘ ω ) ↔ ◡ ( bday ↾ ℕ0s ) : ω –1-1→ ( O ‘ ω ) ) )
61	51 59 60	spcedv	⊢ ( ω ∈ V → ∃ 𝑓 𝑓 : ω –1-1→ ( O ‘ ω ) )
62		fvex	⊢ ( O ‘ ω ) ∈ V
63	62	brdom	⊢ ( ω ≼ ( O ‘ ω ) ↔ ∃ 𝑓 𝑓 : ω –1-1→ ( O ‘ ω ) )
64	61 63	sylibr	⊢ ( ω ∈ V → ω ≼ ( O ‘ ω ) )
65		infinfg	⊢ ( ( ω ∈ V ∧ ( O ‘ ω ) ∈ V ) → ( ¬ ( O ‘ ω ) ∈ Fin ↔ ω ≼ ( O ‘ ω ) ) )
66	62 65	mpan2	⊢ ( ω ∈ V → ( ¬ ( O ‘ ω ) ∈ Fin ↔ ω ≼ ( O ‘ ω ) ) )
67	64 66	mpbird	⊢ ( ω ∈ V → ¬ ( O ‘ ω ) ∈ Fin )
68	45 67	syl	⊢ ( 𝑥 = ω → ¬ ( O ‘ ω ) ∈ Fin )
69	44 68	eqneltrd	⊢ ( 𝑥 = ω → ¬ ( O ‘ 𝑥 ) ∈ Fin )
70	69	con2i	⊢ ( ( O ‘ 𝑥 ) ∈ Fin → ¬ 𝑥 = ω )
71	70	adantl	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ¬ 𝑥 = ω )
72		orel2	⊢ ( ¬ 𝑥 = ω → ( ( 𝑥 ∈ ω ∨ 𝑥 = ω ) → 𝑥 ∈ ω ) )
73	71 72	syl	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( ( 𝑥 ∈ ω ∨ 𝑥 = ω ) → 𝑥 ∈ ω ) )
74	43 73	sylbid	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( 𝑥 ⊆ ω → 𝑥 ∈ ω ) )
75	37 74	syl5	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( ( ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin ) → 𝑥 ∈ ω ) )
76	75	expd	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) → ( ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin → 𝑥 ∈ ω ) ) )
77	76	3impia	⊢ ( ( 𝑥 ∈ On ∧ ( O ‘ 𝑥 ) ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ) → ( ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin → 𝑥 ∈ ω ) )
78	77	3com23	⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑥 ) ∈ Fin ) → ( ∀ 𝑦 ∈ 𝑥 ( O ‘ 𝑦 ) ∈ Fin → 𝑥 ∈ ω ) )
79	30 78	mpd	⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) ∧ ( O ‘ 𝑥 ) ∈ Fin ) → 𝑥 ∈ ω )
80	79	3exp	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( O ‘ 𝑦 ) ∈ Fin → 𝑦 ∈ ω ) → ( ( O ‘ 𝑥 ) ∈ Fin → 𝑥 ∈ ω ) ) )
81	5 9 80	tfis3	⊢ ( 𝐴 ∈ On → ( ( O ‘ 𝐴 ) ∈ Fin → 𝐴 ∈ ω ) )
82	1 81	impbid2	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ ω ↔ ( O ‘ 𝐴 ) ∈ Fin ) )