Metamath Proof Explorer

Theorem onsfi

Description: A surreal ordinal with a finite birthday is a non-negative surreal integer. (Contributed by Scott Fenton, 4-Nov-2025)

Ref Expression
Assertion onsfi ⊢ A ∈ On s ∧ bday ⁡ A ∈ ω → A ∈ ℕ 0s

Proof

Step Hyp Ref Expression
1 risset ⊢ bday ⁡ A ∈ ω ↔ ∃ x ∈ ω x = bday ⁡ A
2 eqeq1 ⊢ y = z → y = bday ⁡ a ↔ z = bday ⁡ a
3 2 imbi1d ⊢ y = z → y = bday ⁡ a → a ∈ ℕ 0s ↔ z = bday ⁡ a → a ∈ ℕ 0s
4 3 ralbidv ⊢ y = z → ∀ a ∈ On s y = bday ⁡ a → a ∈ ℕ 0s ↔ ∀ a ∈ On s z = bday ⁡ a → a ∈ ℕ 0s
5 fveq2 ⊢ a = b → bday ⁡ a = bday ⁡ b
6 5 eqeq2d ⊢ a = b → z = bday ⁡ a ↔ z = bday ⁡ b
7 eleq1 ⊢ a = b → a ∈ ℕ 0s ↔ b ∈ ℕ 0s
8 6 7 imbi12d ⊢ a = b → z = bday ⁡ a → a ∈ ℕ 0s ↔ z = bday ⁡ b → b ∈ ℕ 0s
9 8 cbvralvw ⊢ ∀ a ∈ On s z = bday ⁡ a → a ∈ ℕ 0s ↔ ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s
10 4 9 bitrdi ⊢ y = z → ∀ a ∈ On s y = bday ⁡ a → a ∈ ℕ 0s ↔ ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s
11 eqeq1 ⊢ y = x → y = bday ⁡ a ↔ x = bday ⁡ a
12 11 imbi1d ⊢ y = x → y = bday ⁡ a → a ∈ ℕ 0s ↔ x = bday ⁡ a → a ∈ ℕ 0s
13 12 ralbidv ⊢ y = x → ∀ a ∈ On s y = bday ⁡ a → a ∈ ℕ 0s ↔ ∀ a ∈ On s x = bday ⁡ a → a ∈ ℕ 0s
14 oncutlt ⊢ a ∈ On s → a = x ∈ On s | x < s a | s ∅
15 14 3ad2ant3 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → a = x ∈ On s | x < s a | s ∅
16 onssno ⊢ On s ⊆ No
17 simp13 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → a ∈ On s
18 16 17 sselid ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → a ∈ No
19 ltonold ⊢ a ∈ No → b ∈ On s | b < s a ⊆ Old ⁡ bday ⁡ a
20 18 19 syl ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → b ∈ On s | b < s a ⊆ Old ⁡ bday ⁡ a
21 breq1 ⊢ b = x → b < s a ↔ x < s a
22 simp2 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x ∈ On s
23 simp3 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x < s a
24 21 22 23 elrabd ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x ∈ b ∈ On s | b < s a
25 20 24 sseldd ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x ∈ Old ⁡ bday ⁡ a
26 bdayon ⊢ bday ⁡ a ∈ On
27 16 22 sselid ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x ∈ No
28 oldbday ⊢ bday ⁡ a ∈ On ∧ x ∈ No → x ∈ Old ⁡ bday ⁡ a ↔ bday ⁡ x ∈ bday ⁡ a
29 26 27 28 sylancr ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x ∈ Old ⁡ bday ⁡ a ↔ bday ⁡ x ∈ bday ⁡ a
30 25 29 mpbid ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → bday ⁡ x ∈ bday ⁡ a
31 fveq2 ⊢ b = x → bday ⁡ b = bday ⁡ x
32 31 eleq1d ⊢ b = x → bday ⁡ b ∈ bday ⁡ a ↔ bday ⁡ x ∈ bday ⁡ a
33 eleq1 ⊢ b = x → b ∈ ℕ 0s ↔ x ∈ ℕ 0s
34 32 33 imbi12d ⊢ b = x → bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ↔ bday ⁡ x ∈ bday ⁡ a → x ∈ ℕ 0s
35 simp12 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
36 34 35 22 rspcdva ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → bday ⁡ x ∈ bday ⁡ a → x ∈ ℕ 0s
37 30 36 mpd ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s ∧ x ∈ On s ∧ x < s a → x ∈ ℕ 0s
38 37 rabssdv ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → x ∈ On s | x < s a ⊆ ℕ 0s
39 oldfi ⊢ bday ⁡ a ∈ ω → Old ⁡ bday ⁡ a ∈ Fin
40 39 3ad2ant1 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → Old ⁡ bday ⁡ a ∈ Fin
41 onno ⊢ a ∈ On s → a ∈ No
42 41 3ad2ant3 ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → a ∈ No
43 ltonold ⊢ a ∈ No → x ∈ On s | x < s a ⊆ Old ⁡ bday ⁡ a
44 42 43 syl ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → x ∈ On s | x < s a ⊆ Old ⁡ bday ⁡ a
45 40 44 ssfid ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → x ∈ On s | x < s a ∈ Fin
46 n0fincut ⊢ x ∈ On s | x < s a ⊆ ℕ 0s ∧ x ∈ On s | x < s a ∈ Fin → x ∈ On s | x < s a | s ∅ ∈ ℕ 0s
47 38 45 46 syl2anc ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → x ∈ On s | x < s a | s ∅ ∈ ℕ 0s
48 15 47 eqeltrd ⊢ bday ⁡ a ∈ ω ∧ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s ∧ a ∈ On s → a ∈ ℕ 0s
49 48 3exp ⊢ bday ⁡ a ∈ ω → ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s → a ∈ On s → a ∈ ℕ 0s
50 eleq1 ⊢ y = bday ⁡ a → y ∈ ω ↔ bday ⁡ a ∈ ω
51 raleq ⊢ y = bday ⁡ a → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ z ∈ bday ⁡ a ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s
52 ralcom ⊢ ∀ z ∈ bday ⁡ a ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ b ∈ On s ∀ z ∈ bday ⁡ a z = bday ⁡ b → b ∈ ℕ 0s
53 df-ral ⊢ ∀ z ∈ bday ⁡ a z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ z z ∈ bday ⁡ a → z = bday ⁡ b → b ∈ ℕ 0s
54 bi2.04 ⊢ z ∈ bday ⁡ a → z = bday ⁡ b → b ∈ ℕ 0s ↔ z = bday ⁡ b → z ∈ bday ⁡ a → b ∈ ℕ 0s
55 54 albii ⊢ ∀ z z ∈ bday ⁡ a → z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ z z = bday ⁡ b → z ∈ bday ⁡ a → b ∈ ℕ 0s
56 fvex ⊢ bday ⁡ b ∈ V
57 eleq1 ⊢ z = bday ⁡ b → z ∈ bday ⁡ a ↔ bday ⁡ b ∈ bday ⁡ a
58 57 imbi1d ⊢ z = bday ⁡ b → z ∈ bday ⁡ a → b ∈ ℕ 0s ↔ bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
59 56 58 ceqsalv ⊢ ∀ z z = bday ⁡ b → z ∈ bday ⁡ a → b ∈ ℕ 0s ↔ bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
60 53 55 59 3bitri ⊢ ∀ z ∈ bday ⁡ a z = bday ⁡ b → b ∈ ℕ 0s ↔ bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
61 60 ralbii ⊢ ∀ b ∈ On s ∀ z ∈ bday ⁡ a z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
62 52 61 bitri ⊢ ∀ z ∈ bday ⁡ a ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
63 51 62 bitrdi ⊢ y = bday ⁡ a → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s ↔ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s
64 63 imbi1d ⊢ y = bday ⁡ a → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s → a ∈ On s → a ∈ ℕ 0s ↔ ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s → a ∈ On s → a ∈ ℕ 0s
65 50 64 imbi12d ⊢ y = bday ⁡ a → y ∈ ω → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s → a ∈ On s → a ∈ ℕ 0s ↔ bday ⁡ a ∈ ω → ∀ b ∈ On s bday ⁡ b ∈ bday ⁡ a → b ∈ ℕ 0s → a ∈ On s → a ∈ ℕ 0s
66 49 65 mpbiri ⊢ y = bday ⁡ a → y ∈ ω → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s → a ∈ On s → a ∈ ℕ 0s
67 66 com4l ⊢ y ∈ ω → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s → a ∈ On s → y = bday ⁡ a → a ∈ ℕ 0s
68 67 ralrimdv ⊢ y ∈ ω → ∀ z ∈ y ∀ b ∈ On s z = bday ⁡ b → b ∈ ℕ 0s → ∀ a ∈ On s y = bday ⁡ a → a ∈ ℕ 0s
69 10 13 68 omsinds ⊢ x ∈ ω → ∀ a ∈ On s x = bday ⁡ a → a ∈ ℕ 0s
70 fveq2 ⊢ a = A → bday ⁡ a = bday ⁡ A
71 70 eqeq2d ⊢ a = A → x = bday ⁡ a ↔ x = bday ⁡ A
72 eleq1 ⊢ a = A → a ∈ ℕ 0s ↔ A ∈ ℕ 0s
73 71 72 imbi12d ⊢ a = A → x = bday ⁡ a → a ∈ ℕ 0s ↔ x = bday ⁡ A → A ∈ ℕ 0s
74 73 rspccv ⊢ ∀ a ∈ On s x = bday ⁡ a → a ∈ ℕ 0s → A ∈ On s → x = bday ⁡ A → A ∈ ℕ 0s
75 69 74 syl ⊢ x ∈ ω → A ∈ On s → x = bday ⁡ A → A ∈ ℕ 0s
76 75 com23 ⊢ x ∈ ω → x = bday ⁡ A → A ∈ On s → A ∈ ℕ 0s
77 76 rexlimiv ⊢ ∃ x ∈ ω x = bday ⁡ A → A ∈ On s → A ∈ ℕ 0s
78 1 77 sylbi ⊢ bday ⁡ A ∈ ω → A ∈ On s → A ∈ ℕ 0s
79 78 impcom ⊢ A ∈ On s ∧ bday ⁡ A ∈ ω → A ∈ ℕ 0s