Metamath Proof Explorer

Theorem n0sbday

Description: A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Assertion n0sbday 
|- ( A e. NN0_s -> ( bday ` A ) e. _om )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( m = 0s -> ( bday ` m ) = ( bday ` 0s ) )
2 1 eleq1d 
 |-  ( m = 0s -> ( ( bday ` m ) e. _om <-> ( bday ` 0s ) e. _om ) )
3 fveq2 
 |-  ( m = n -> ( bday ` m ) = ( bday ` n ) )
4 3 eleq1d 
 |-  ( m = n -> ( ( bday ` m ) e. _om <-> ( bday ` n ) e. _om ) )
5 fveq2 
 |-  ( m = ( n +s 1s ) -> ( bday ` m ) = ( bday ` ( n +s 1s ) ) )
6 5 eleq1d 
 |-  ( m = ( n +s 1s ) -> ( ( bday ` m ) e. _om <-> ( bday ` ( n +s 1s ) ) e. _om ) )
7 fveq2 
 |-  ( m = A -> ( bday ` m ) = ( bday ` A ) )
8 7 eleq1d 
 |-  ( m = A -> ( ( bday ` m ) e. _om <-> ( bday ` A ) e. _om ) )
9 bday0s 
 |-  ( bday ` 0s ) = (/)
10 peano1 
 |-  (/) e. _om
11 9 10 eqeltri 
 |-  ( bday ` 0s ) e. _om
12 n0scut2 
 |-  ( n e. NN0_s -> ( n +s 1s ) = ( { n } |s (/) ) )
13 12 fveq2d 
 |-  ( n e. NN0_s -> ( bday ` ( n +s 1s ) ) = ( bday ` ( { n } |s (/) ) ) )
14 n0sno 
 |-  ( n e. NN0_s -> n e. No )
15 snelpwi 
 |-  ( n e. No -> { n } e. ~P No )
16 nulssgt 
 |-  ( { n } e. ~P No -> { n } <
17 14 15 16 3syl 
 |-  ( n e. NN0_s -> { n } <
18 un0 
 |-  ( { n } u. (/) ) = { n }
19 18 imaeq2i 
 |-  ( bday " ( { n } u. (/) ) ) = ( bday " { n } )
20 bdayfn 
 |-  bday Fn No
21 fnsnfv 
 |-  ( ( bday Fn No /\ n e. No ) -> { ( bday ` n ) } = ( bday " { n } ) )
22 20 14 21 sylancr 
 |-  ( n e. NN0_s -> { ( bday ` n ) } = ( bday " { n } ) )
23 19 22 eqtr4id 
 |-  ( n e. NN0_s -> ( bday " ( { n } u. (/) ) ) = { ( bday ` n ) } )
24 fvex 
 |-  ( bday ` n ) e. _V
25 24 sucid 
 |-  ( bday ` n ) e. suc ( bday ` n )
26 snssi 
 |-  ( ( bday ` n ) e. suc ( bday ` n ) -> { ( bday ` n ) } C_ suc ( bday ` n ) )
27 25 26 ax-mp 
 |-  { ( bday ` n ) } C_ suc ( bday ` n )
28 23 27 eqsstrdi 
 |-  ( n e. NN0_s -> ( bday " ( { n } u. (/) ) ) C_ suc ( bday ` n ) )
29 bdayelon 
 |-  ( bday ` n ) e. On
30 29 onsuci 
 |-  suc ( bday ` n ) e. On
31 scutbdaybnd 
 |-  ( ( { n } < ( bday ` ( { n } |s (/) ) ) C_ suc ( bday ` n ) )
32 30 31 mp3an2 
 |-  ( ( { n } < ( bday ` ( { n } |s (/) ) ) C_ suc ( bday ` n ) )
33 17 28 32 syl2anc 
 |-  ( n e. NN0_s -> ( bday ` ( { n } |s (/) ) ) C_ suc ( bday ` n ) )
34 13 33 eqsstrd 
 |-  ( n e. NN0_s -> ( bday ` ( n +s 1s ) ) C_ suc ( bday ` n ) )
35 bdayelon 
 |-  ( bday ` ( n +s 1s ) ) e. On
36 onsssuc 
 |-  ( ( ( bday ` ( n +s 1s ) ) e. On /\ suc ( bday ` n ) e. On ) -> ( ( bday ` ( n +s 1s ) ) C_ suc ( bday ` n ) <-> ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) ) )
37 35 30 36 mp2an 
 |-  ( ( bday ` ( n +s 1s ) ) C_ suc ( bday ` n ) <-> ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) )
38 34 37 sylib 
 |-  ( n e. NN0_s -> ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) )
39 peano2 
 |-  ( ( bday ` n ) e. _om -> suc ( bday ` n ) e. _om )
40 peano2 
 |-  ( suc ( bday ` n ) e. _om -> suc suc ( bday ` n ) e. _om )
41 39 40 syl 
 |-  ( ( bday ` n ) e. _om -> suc suc ( bday ` n ) e. _om )
42 elnn 
 |-  ( ( ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) /\ suc suc ( bday ` n ) e. _om ) -> ( bday ` ( n +s 1s ) ) e. _om )
43 38 41 42 syl2an 
 |-  ( ( n e. NN0_s /\ ( bday ` n ) e. _om ) -> ( bday ` ( n +s 1s ) ) e. _om )
44 43 ex 
 |-  ( n e. NN0_s -> ( ( bday ` n ) e. _om -> ( bday ` ( n +s 1s ) ) e. _om ) )
45 2 4 6 8 11 44 n0sind 
 |-  ( A e. NN0_s -> ( bday ` A ) e. _om )