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 ⊢ A ∈ No → bday ⁡ A = ⋃ x ∈ Old ⁡ bday ⁡ A suc ⁡ bday ⁡ x

Proof

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