Metamath Proof Explorer

Theorem bdayn0sf1o

Description: The birthday function restricted to the non-negative surreal integers is a bijection with the finite ordinals. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion bdayn0sf1o ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω

Proof

Step Hyp Ref Expression
1 bdayfun ⊢ Fun bday
2 funres ⊢ ( Fun bday → Fun ( bday ↾ ℕ0s ) )
3 1 2 ax-mp ⊢ Fun ( bday ↾ ℕ0s )
4 dmres ⊢ dom ( bday ↾ ℕ0s ) = ( ℕ0s ∩ dom bday )
5 bdaydm ⊢ dom bday = No
6 5 ineq2i ⊢ ( ℕ0s ∩ dom bday ) = ( ℕ0s ∩ No )
7 n0ssno ⊢ ℕ0s ⊆ No
8 dfss2 ⊢ ( ℕ0s ⊆ No ↔ ( ℕ0s ∩ No ) = ℕ0s )
9 7 8 mpbi ⊢ ( ℕ0s ∩ No ) = ℕ0s
10 4 6 9 3eqtri ⊢ dom ( bday ↾ ℕ0s ) = ℕ0s
11 df-fn ⊢ ( ( bday ↾ ℕ0s ) Fn ℕ0s ↔ ( Fun ( bday ↾ ℕ0s ) ∧ dom ( bday ↾ ℕ0s ) = ℕ0s ) )
12 3 10 11 mpbir2an ⊢ ( bday ↾ ℕ0s ) Fn ℕ0s
13 fvres ⊢ ( 𝑥 ∈ ℕ0s → ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) = ( bday ‘ 𝑥 ) )
14 n0bday ⊢ ( 𝑥 ∈ ℕ0s → ( bday ‘ 𝑥 ) ∈ ω )
15 13 14 eqeltrd ⊢ ( 𝑥 ∈ ℕ0s → ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) ∈ ω )
16 15 rgen ⊢ ∀ 𝑥 ∈ ℕ0s ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) ∈ ω
17 fnfvrnss ⊢ ( ( ( bday ↾ ℕ0s ) Fn ℕ0s ∧ ∀ 𝑥 ∈ ℕ0s ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) ∈ ω ) → ran ( bday ↾ ℕ0s ) ⊆ ω )
18 12 16 17 mp2an ⊢ ran ( bday ↾ ℕ0s ) ⊆ ω
19 eqeq2 ⊢ ( 𝑏 = ∅ → ( ( bday ‘ 𝑦 ) = 𝑏 ↔ ( bday ‘ 𝑦 ) = ∅ ) )
20 19 rexbidv ⊢ ( 𝑏 = ∅ → ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑏 ↔ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = ∅ ) )
21 eqeq2 ⊢ ( 𝑏 = 𝑎 → ( ( bday ‘ 𝑦 ) = 𝑏 ↔ ( bday ‘ 𝑦 ) = 𝑎 ) )
22 21 rexbidv ⊢ ( 𝑏 = 𝑎 → ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑏 ↔ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑎 ) )
23 eqeq2 ⊢ ( 𝑏 = suc 𝑎 → ( ( bday ‘ 𝑦 ) = 𝑏 ↔ ( bday ‘ 𝑦 ) = suc 𝑎 ) )
24 23 rexbidv ⊢ ( 𝑏 = suc 𝑎 → ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑏 ↔ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = suc 𝑎 ) )
25 fveqeq2 ⊢ ( 𝑦 = 𝑧 → ( ( bday ‘ 𝑦 ) = suc 𝑎 ↔ ( bday ‘ 𝑧 ) = suc 𝑎 ) )
26 25 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = suc 𝑎 ↔ ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc 𝑎 )
27 24 26 bitrdi ⊢ ( 𝑏 = suc 𝑎 → ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑏 ↔ ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc 𝑎 ) )
28 eqeq2 ⊢ ( 𝑏 = 𝑥 → ( ( bday ‘ 𝑦 ) = 𝑏 ↔ ( bday ‘ 𝑦 ) = 𝑥 ) )
29 28 rexbidv ⊢ ( 𝑏 = 𝑥 → ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑏 ↔ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑥 ) )
30 0n0s ⊢ 0s ∈ ℕ0s
31 bday0 ⊢ ( bday ‘ 0s ) = ∅
32 fveqeq2 ⊢ ( 𝑦 = 0s → ( ( bday ‘ 𝑦 ) = ∅ ↔ ( bday ‘ 0s ) = ∅ ) )
33 32 rspcev ⊢ ( ( 0s ∈ ℕ0s ∧ ( bday ‘ 0s ) = ∅ ) → ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = ∅ )
34 30 31 33 mp2an ⊢ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = ∅
35 fveqeq2 ⊢ ( 𝑧 = ( 𝑦 +s 1s ) → ( ( bday ‘ 𝑧 ) = suc ( bday ‘ 𝑦 ) ↔ ( bday ‘ ( 𝑦 +s 1s ) ) = suc ( bday ‘ 𝑦 ) ) )
36 peano2n0s ⊢ ( 𝑦 ∈ ℕ0s → ( 𝑦 +s 1s ) ∈ ℕ0s )
37 bdayn0p1 ⊢ ( 𝑦 ∈ ℕ0s → ( bday ‘ ( 𝑦 +s 1s ) ) = suc ( bday ‘ 𝑦 ) )
38 35 36 37 rspcedvdw ⊢ ( 𝑦 ∈ ℕ0s → ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc ( bday ‘ 𝑦 ) )
39 38 adantl ⊢ ( ( 𝑎 ∈ ω ∧ 𝑦 ∈ ℕ0s ) → ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc ( bday ‘ 𝑦 ) )
40 suceq ⊢ ( ( bday ‘ 𝑦 ) = 𝑎 → suc ( bday ‘ 𝑦 ) = suc 𝑎 )
41 40 eqeq2d ⊢ ( ( bday ‘ 𝑦 ) = 𝑎 → ( ( bday ‘ 𝑧 ) = suc ( bday ‘ 𝑦 ) ↔ ( bday ‘ 𝑧 ) = suc 𝑎 ) )
42 41 rexbidv ⊢ ( ( bday ‘ 𝑦 ) = 𝑎 → ( ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc ( bday ‘ 𝑦 ) ↔ ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc 𝑎 ) )
43 39 42 syl5ibcom ⊢ ( ( 𝑎 ∈ ω ∧ 𝑦 ∈ ℕ0s ) → ( ( bday ‘ 𝑦 ) = 𝑎 → ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc 𝑎 ) )
44 43 rexlimdva ⊢ ( 𝑎 ∈ ω → ( ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑎 → ∃ 𝑧 ∈ ℕ0s ( bday ‘ 𝑧 ) = suc 𝑎 ) )
45 20 22 27 29 34 44 finds ⊢ ( 𝑥 ∈ ω → ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑥 )
46 fvelrnb ⊢ ( ( bday ↾ ℕ0s ) Fn ℕ0s → ( 𝑥 ∈ ran ( bday ↾ ℕ0s ) ↔ ∃ 𝑦 ∈ ℕ0s ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) = 𝑥 ) )
47 12 46 ax-mp ⊢ ( 𝑥 ∈ ran ( bday ↾ ℕ0s ) ↔ ∃ 𝑦 ∈ ℕ0s ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) = 𝑥 )
48 fvres ⊢ ( 𝑦 ∈ ℕ0s → ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) = ( bday ‘ 𝑦 ) )
49 48 eqeq1d ⊢ ( 𝑦 ∈ ℕ0s → ( ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) = 𝑥 ↔ ( bday ‘ 𝑦 ) = 𝑥 ) )
50 49 rexbiia ⊢ ( ∃ 𝑦 ∈ ℕ0s ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑥 )
51 47 50 bitri ⊢ ( 𝑥 ∈ ran ( bday ↾ ℕ0s ) ↔ ∃ 𝑦 ∈ ℕ0s ( bday ‘ 𝑦 ) = 𝑥 )
52 45 51 sylibr ⊢ ( 𝑥 ∈ ω → 𝑥 ∈ ran ( bday ↾ ℕ0s ) )
53 52 ssriv ⊢ ω ⊆ ran ( bday ↾ ℕ0s )
54 18 53 eqssi ⊢ ran ( bday ↾ ℕ0s ) = ω
55 df-fo ⊢ ( ( bday ↾ ℕ0s ) : ℕ0s –onto→ ω ↔ ( ( bday ↾ ℕ0s ) Fn ℕ0s ∧ ran ( bday ↾ ℕ0s ) = ω ) )
56 12 54 55 mpbir2an ⊢ ( bday ↾ ℕ0s ) : ℕ0s –onto→ ω
57 fof ⊢ ( ( bday ↾ ℕ0s ) : ℕ0s –onto→ ω → ( bday ↾ ℕ0s ) : ℕ0s ⟶ ω )
58 56 57 ax-mp ⊢ ( bday ↾ ℕ0s ) : ℕ0s ⟶ ω
59 13 48 eqeqan12d ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → ( ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) = ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) ↔ ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) ) )
60 n0on ⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ Ons )
61 n0on ⊢ ( 𝑦 ∈ ℕ0s → 𝑦 ∈ Ons )
62 bday11on ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ∧ ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
63 62 3expia ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
64 60 61 63 syl2an ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → ( ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
65 59 64 sylbid ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → ( ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) = ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
66 65 rgen2 ⊢ ∀ 𝑥 ∈ ℕ0s ∀ 𝑦 ∈ ℕ0s ( ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) = ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) → 𝑥 = 𝑦 )
67 dff13 ⊢ ( ( bday ↾ ℕ0s ) : ℕ0s –1-1→ ω ↔ ( ( bday ↾ ℕ0s ) : ℕ0s ⟶ ω ∧ ∀ 𝑥 ∈ ℕ0s ∀ 𝑦 ∈ ℕ0s ( ( ( bday ↾ ℕ0s ) ‘ 𝑥 ) = ( ( bday ↾ ℕ0s ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
68 58 66 67 mpbir2an ⊢ ( bday ↾ ℕ0s ) : ℕ0s –1-1→ ω
69 df-f1o ⊢ ( ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω ↔ ( ( bday ↾ ℕ0s ) : ℕ0s –1-1→ ω ∧ ( bday ↾ ℕ0s ) : ℕ0s –onto→ ω ) )
70 68 56 69 mpbir2an ⊢ ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω