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 e. No -> ( bday ` A ) = U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )

Proof

Step Hyp Ref Expression
1 lrcut 
 |-  ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
2 1 fveq2d 
 |-  ( A e. No -> ( bday ` ( ( _Left ` A ) |s ( _Right ` A ) ) ) = ( bday ` A ) )
3 lltropt 
 |-  ( _Left ` A ) <
4 fvex 
 |-  ( _Old ` ( bday ` A ) ) e. _V
5 bdayelon 
 |-  ( bday ` x ) e. On
6 5 onsuci 
 |-  suc ( bday ` x ) e. On
7 6 rgenw 
 |-  A. x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) e. On
8 iunon 
 |-  ( ( ( _Old ` ( bday ` A ) ) e. _V /\ A. x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) e. On ) -> U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) e. On )
9 4 7 8 mp2an 
 |-  U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) e. On
10 lrold 
 |-  ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) )
11 10 imaeq2i 
 |-  ( bday " ( ( _Left ` A ) u. ( _Right ` A ) ) ) = ( bday " ( _Old ` ( bday ` A ) ) )
12 nfv 
 |-  F/ y A e. No
13 bdayfun 
 |-  Fun bday
14 13 a1i 
 |-  ( A e. No -> Fun bday )
15 fvex 
 |-  ( bday ` y ) e. _V
16 15 sucid 
 |-  ( bday ` y ) e. 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 ) e. suc ( bday ` x ) <-> ( bday ` y ) e. suc ( bday ` y ) ) )
20 19 rspcev 
 |-  ( ( y e. ( _Old ` ( bday ` A ) ) /\ ( bday ` y ) e. suc ( bday ` y ) ) -> E. x e. ( _Old ` ( bday ` A ) ) ( bday ` y ) e. suc ( bday ` x ) )
21 16 20 mpan2 
 |-  ( y e. ( _Old ` ( bday ` A ) ) -> E. x e. ( _Old ` ( bday ` A ) ) ( bday ` y ) e. suc ( bday ` x ) )
22 21 adantl 
 |-  ( ( A e. No /\ y e. ( _Old ` ( bday ` A ) ) ) -> E. x e. ( _Old ` ( bday ` A ) ) ( bday ` y ) e. suc ( bday ` x ) )
23 22 eliund 
 |-  ( ( A e. No /\ y e. ( _Old ` ( bday ` A ) ) ) -> ( bday ` y ) e. U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )
24 12 14 23 funimassd 
 |-  ( A e. No -> ( bday " ( _Old ` ( bday ` A ) ) ) C_ U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )
25 11 24 eqsstrid 
 |-  ( A e. No -> ( bday " ( ( _Left ` A ) u. ( _Right ` A ) ) ) C_ U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )
26 scutbdaybnd 
 |-  ( ( ( _Left ` A ) < ( bday ` ( ( _Left ` A ) |s ( _Right ` A ) ) ) C_ U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )
27 3 9 25 26 mp3an12i 
 |-  ( A e. No -> ( bday ` ( ( _Left ` A ) |s ( _Right ` A ) ) ) C_ U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )
28 2 27 eqsstrrd 
 |-  ( A e. No -> ( bday ` A ) C_ U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )
29 oldbdayim 
 |-  ( x e. ( _Old ` ( bday ` A ) ) -> ( bday ` x ) e. ( bday ` A ) )
30 29 adantl 
 |-  ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( bday ` x ) e. ( bday ` A ) )
31 bdayelon 
 |-  ( bday ` A ) e. On
32 5 31 onsucssi 
 |-  ( ( bday ` x ) e. ( bday ` A ) <-> suc ( bday ` x ) C_ ( bday ` A ) )
33 30 32 sylib 
 |-  ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> suc ( bday ` x ) C_ ( bday ` A ) )
34 33 iunssd 
 |-  ( A e. No -> U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) C_ ( bday ` A ) )
35 28 34 eqssd 
 |-  ( A e. No -> ( bday ` A ) = U_ x e. ( _Old ` ( bday ` A ) ) suc ( bday ` x ) )