Metamath Proof Explorer

Theorem bdayn0p1

Description: The birthday of A +s 1s is the successor of the birthday of A when A is a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion bdayn0p1 
|- ( A e. NN0_s -> ( bday ` ( A +s 1s ) ) = suc ( bday ` A ) )

Proof

Step Hyp Ref Expression
1 n0scut2 
 |-  ( A e. NN0_s -> ( A +s 1s ) = ( { A } |s (/) ) )
2 1 fveq2d 
 |-  ( A e. NN0_s -> ( bday ` ( A +s 1s ) ) = ( bday ` ( { A } |s (/) ) ) )
3 n0sno 
 |-  ( A e. NN0_s -> A e. No )
4 snelpwi 
 |-  ( A e. No -> { A } e. ~P No )
5 nulssgt 
 |-  ( { A } e. ~P No -> { A } <
6 3 4 5 3syl 
 |-  ( A e. NN0_s -> { A } <
7 un0 
 |-  ( { A } u. (/) ) = { A }
8 7 imaeq2i 
 |-  ( bday " ( { A } u. (/) ) ) = ( bday " { A } )
9 bdayfn 
 |-  bday Fn No
10 9 a1i 
 |-  ( A e. NN0_s -> bday Fn No )
11 10 3 fnimasnd 
 |-  ( A e. NN0_s -> ( bday " { A } ) = { ( bday ` A ) } )
12 ssun2 
 |-  { ( bday ` A ) } C_ ( ( bday ` A ) u. { ( bday ` A ) } )
13 df-suc 
 |-  suc ( bday ` A ) = ( ( bday ` A ) u. { ( bday ` A ) } )
14 12 13 sseqtrri 
 |-  { ( bday ` A ) } C_ suc ( bday ` A )
15 11 14 eqsstrdi 
 |-  ( A e. NN0_s -> ( bday " { A } ) C_ suc ( bday ` A ) )
16 8 15 eqsstrid 
 |-  ( A e. NN0_s -> ( bday " ( { A } u. (/) ) ) C_ suc ( bday ` A ) )
17 bdayelon 
 |-  ( bday ` A ) e. On
18 onsuc 
 |-  ( ( bday ` A ) e. On -> suc ( bday ` A ) e. On )
19 17 18 ax-mp 
 |-  suc ( bday ` A ) e. On
20 scutbdaybnd 
 |-  ( ( { A } < ( bday ` ( { A } |s (/) ) ) C_ suc ( bday ` A ) )
21 19 20 mp3an2 
 |-  ( ( { A } < ( bday ` ( { A } |s (/) ) ) C_ suc ( bday ` A ) )
22 6 16 21 syl2anc 
 |-  ( A e. NN0_s -> ( bday ` ( { A } |s (/) ) ) C_ suc ( bday ` A ) )
23 ssltsep 
 |-  ( { A } < A. x e. { A } A. y e. { z } x
24 breq1 
 |-  ( x = A -> ( x  A
25 24 ralbidv 
 |-  ( x = A -> ( A. y e. { z } x  A. y e. { z } A
26 vex 
 |-  z e. _V
27 breq2 
 |-  ( y = z -> ( A  A
28 26 27 ralsn 
 |-  ( A. y e. { z } A  A
29 25 28 bitrdi 
 |-  ( x = A -> ( A. y e. { z } x  A
30 29 ralsng 
 |-  ( A e. NN0_s -> ( A. x e. { A } A. y e. { z } x  A
31 30 adantr 
 |-  ( ( A e. NN0_s /\ z e. No ) -> ( A. x e. { A } A. y e. { z } x  A
32 n0ons 
 |-  ( A e. NN0_s -> A e. On_s )
33 onnolt 
 |-  ( ( A e. On_s /\ z e. No /\ A  ( bday ` A ) e. ( bday ` z ) )
34 32 33 syl3an1 
 |-  ( ( A e. NN0_s /\ z e. No /\ A  ( bday ` A ) e. ( bday ` z ) )
35 34 3expia 
 |-  ( ( A e. NN0_s /\ z e. No ) -> ( A  ( bday ` A ) e. ( bday ` z ) ) )
36 31 35 sylbid 
 |-  ( ( A e. NN0_s /\ z e. No ) -> ( A. x e. { A } A. y e. { z } x  ( bday ` A ) e. ( bday ` z ) ) )
37 23 36 syl5 
 |-  ( ( A e. NN0_s /\ z e. No ) -> ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
38 37 adantrd 
 |-  ( ( A e. NN0_s /\ z e. No ) -> ( ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
39 38 ralrimiva 
 |-  ( A e. NN0_s -> A. z e. No ( ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
40 ssint 
 |-  ( suc ( bday ` A ) C_ |^| ( bday " { x e. No | ( { A } < A. y e. ( bday " { x e. No | ( { A } <
41 ssrab2 
 |-  { x e. No | ( { A } <
42 sseq2 
 |-  ( y = ( bday ` z ) -> ( suc ( bday ` A ) C_ y <-> suc ( bday ` A ) C_ ( bday ` z ) ) )
43 42 ralima 
 |-  ( ( bday Fn No /\ { x e. No | ( { A } < ( A. y e. ( bday " { x e. No | ( { A } < A. z e. { x e. No | ( { A } <
44 9 41 43 mp2an 
 |-  ( A. y e. ( bday " { x e. No | ( { A } < A. z e. { x e. No | ( { A } <
45 bdayelon 
 |-  ( bday ` z ) e. On
46 17 45 onsucssi 
 |-  ( ( bday ` A ) e. ( bday ` z ) <-> suc ( bday ` A ) C_ ( bday ` z ) )
47 46 ralbii 
 |-  ( A. z e. { x e. No | ( { A } < A. z e. { x e. No | ( { A } <
48 sneq 
 |-  ( x = z -> { x } = { z } )
49 48 breq2d 
 |-  ( x = z -> ( { A } < { A } <
50 48 breq1d 
 |-  ( x = z -> ( { x } < { z } <
51 49 50 anbi12d 
 |-  ( x = z -> ( ( { A } < ( { A } <
52 51 ralrab 
 |-  ( A. z e. { x e. No | ( { A } < A. z e. No ( ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
53 47 52 bitr3i 
 |-  ( A. z e. { x e. No | ( { A } < A. z e. No ( ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
54 44 53 bitri 
 |-  ( A. y e. ( bday " { x e. No | ( { A } < A. z e. No ( ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
55 40 54 bitri 
 |-  ( suc ( bday ` A ) C_ |^| ( bday " { x e. No | ( { A } < A. z e. No ( ( { A } < ( bday ` A ) e. ( bday ` z ) ) )
56 39 55 sylibr 
 |-  ( A e. NN0_s -> suc ( bday ` A ) C_ |^| ( bday " { x e. No | ( { A } <
57 scutbday 
 |-  ( { A } < ( bday ` ( { A } |s (/) ) ) = |^| ( bday " { x e. No | ( { A } <
58 6 57 syl 
 |-  ( A e. NN0_s -> ( bday ` ( { A } |s (/) ) ) = |^| ( bday " { x e. No | ( { A } <
59 56 58 sseqtrrd 
 |-  ( A e. NN0_s -> suc ( bday ` A ) C_ ( bday ` ( { A } |s (/) ) ) )
60 22 59 eqssd 
 |-  ( A e. NN0_s -> ( bday ` ( { A } |s (/) ) ) = suc ( bday ` A ) )
61 2 60 eqtrd 
 |-  ( A e. NN0_s -> ( bday ` ( A +s 1s ) ) = suc ( bday ` A ) )