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 ( ( 𝐴 ∈ Ons ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 𝐴 ∈ ℕ0s )

Proof

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