Metamath Proof Explorer

Theorem bdayiun

Description: The birthday of a surreal is the least upper bound of the successors of the birthdays of its options. This is the definition of the birthday of a combinatorial game in the Lean Combinatorial Game Theory library at https://github.com/vihdzp/combinatorial-games . (Contributed by Scott Fenton, 22-Nov-2025)

Ref Expression
Assertion bdayiun ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 lrcut ⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
2 1 fveq2d ⊢ ( 𝐴 ∈ No → ( bday ‘ ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) ) = ( bday ‘ 𝐴 ) )
3 lltropt ⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
4 fvex ⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ∈ V
5 bdayelon ⊢ ( bday ‘ 𝑥 ) ∈ On
6 5 onsuci ⊢ suc ( bday ‘ 𝑥 ) ∈ On
7 6 rgenw ⊢ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ∈ On
8 iunon ⊢ ( ( ( O ‘ ( bday ‘ 𝐴 ) ) ∈ V ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ∈ On ) → ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ∈ On )
9 4 7 8 mp2an ⊢ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ∈ On
10 lrold ⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) )
11 10 imaeq2i ⊢ ( bday “ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) = ( bday “ ( O ‘ ( bday ‘ 𝐴 ) ) )
12 nfv ⊢ Ⅎ 𝑦 𝐴 ∈ No
13 bdayfun ⊢ Fun bday
14 13 a1i ⊢ ( 𝐴 ∈ No → Fun bday )
15 fvex ⊢ ( bday ‘ 𝑦 ) ∈ V
16 15 sucid ⊢ ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑦 )
17 fveq2 ⊢ ( 𝑥 = 𝑦 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) )
18 17 suceqd ⊢ ( 𝑥 = 𝑦 → suc ( bday ‘ 𝑥 ) = suc ( bday ‘ 𝑦 ) )
19 18 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑥 ) ↔ ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑦 ) ) )
20 19 rspcev ⊢ ( ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑥 ) )
21 16 20 mpan2 ⊢ ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑥 ) )
22 21 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ∃ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ( bday ‘ 𝑦 ) ∈ suc ( bday ‘ 𝑥 ) )
23 22 eliund ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )
24 12 14 23 funimassd ⊢ ( 𝐴 ∈ No → ( bday “ ( O ‘ ( bday ‘ 𝐴 ) ) ) ⊆ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )
25 11 24 eqsstrid ⊢ ( 𝐴 ∈ No → ( bday “ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ⊆ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )
26 scutbdaybnd ⊢ ( ( ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) ∧ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ∈ On ∧ ( bday “ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ⊆ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ) → ( bday ‘ ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) ) ⊆ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )
27 3 9 25 26 mp3an12i ⊢ ( 𝐴 ∈ No → ( bday ‘ ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) ) ⊆ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )
28 2 27 eqsstrrd ⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )
29 oldbdayim ⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) )
30 29 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) )
31 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
32 5 31 onsucssi ⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ↔ suc ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐴 ) )
33 30 32 sylib ⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → suc ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐴 ) )
34 33 iunssd ⊢ ( 𝐴 ∈ No → ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐴 ) )
35 28 34 eqssd ⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ∪ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) suc ( bday ‘ 𝑥 ) )