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	$⊢ A \in On \to (A \in ω \leftrightarrow Old (A) \in Fin)$

Proof

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

Metamath Proof Explorer

Theorem oldfib

Proof