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 peano2n0s 
 |-  ( n e. NN0_s -> ( n +s 1s ) e. NN0_s )
13 n0scut 
 |-  ( ( n +s 1s ) e. NN0_s -> ( n +s 1s ) = ( { ( ( n +s 1s ) -s 1s ) } |s (/) ) )
14 12 13 syl 
 |-  ( n e. NN0_s -> ( n +s 1s ) = ( { ( ( n +s 1s ) -s 1s ) } |s (/) ) )
15 n0sno 
 |-  ( n e. NN0_s -> n e. No )
16 1sno 
 |-  1s e. No
17 pncans 
 |-  ( ( n e. No /\ 1s e. No ) -> ( ( n +s 1s ) -s 1s ) = n )
18 15 16 17 sylancl 
 |-  ( n e. NN0_s -> ( ( n +s 1s ) -s 1s ) = n )
19 18 sneqd 
 |-  ( n e. NN0_s -> { ( ( n +s 1s ) -s 1s ) } = { n } )
20 19 oveq1d 
 |-  ( n e. NN0_s -> ( { ( ( n +s 1s ) -s 1s ) } |s (/) ) = ( { n } |s (/) ) )
21 14 20 eqtrd 
 |-  ( n e. NN0_s -> ( n +s 1s ) = ( { n } |s (/) ) )
22 21 fveq2d 
 |-  ( n e. NN0_s -> ( bday ` ( n +s 1s ) ) = ( bday ` ( { n } |s (/) ) ) )
23 snelpwi 
 |-  ( n e. No -> { n } e. ~P No )
24 nulssgt 
 |-  ( { n } e. ~P No -> { n } <
25 15 23 24 3syl 
 |-  ( n e. NN0_s -> { n } <
26 un0 
 |-  ( { n } u. (/) ) = { n }
27 26 imaeq2i 
 |-  ( bday " ( { n } u. (/) ) ) = ( bday " { n } )
28 bdayfn 
 |-  bday Fn No
29 fnsnfv 
 |-  ( ( bday Fn No /\ n e. No ) -> { ( bday ` n ) } = ( bday " { n } ) )
30 28 15 29 sylancr 
 |-  ( n e. NN0_s -> { ( bday ` n ) } = ( bday " { n } ) )
31 27 30 eqtr4id 
 |-  ( n e. NN0_s -> ( bday " ( { n } u. (/) ) ) = { ( bday ` n ) } )
32 fvex 
 |-  ( bday ` n ) e. _V
33 32 sucid 
 |-  ( bday ` n ) e. suc ( bday ` n )
34 snssi 
 |-  ( ( bday ` n ) e. suc ( bday ` n ) -> { ( bday ` n ) } C_ suc ( bday ` n ) )
35 33 34 ax-mp 
 |-  { ( bday ` n ) } C_ suc ( bday ` n )
36 31 35 eqsstrdi 
 |-  ( n e. NN0_s -> ( bday " ( { n } u. (/) ) ) C_ suc ( bday ` n ) )
37 bdayelon 
 |-  ( bday ` n ) e. On
38 37 onsuci 
 |-  suc ( bday ` n ) e. On
39 scutbdaybnd 
 |-  ( ( { n } < ( bday ` ( { n } |s (/) ) ) C_ suc ( bday ` n ) )
40 38 39 mp3an2 
 |-  ( ( { n } < ( bday ` ( { n } |s (/) ) ) C_ suc ( bday ` n ) )
41 25 36 40 syl2anc 
 |-  ( n e. NN0_s -> ( bday ` ( { n } |s (/) ) ) C_ suc ( bday ` n ) )
42 22 41 eqsstrd 
 |-  ( n e. NN0_s -> ( bday ` ( n +s 1s ) ) C_ suc ( bday ` n ) )
43 bdayelon 
 |-  ( bday ` ( n +s 1s ) ) e. On
44 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 ) ) )
45 43 38 44 mp2an 
 |-  ( ( bday ` ( n +s 1s ) ) C_ suc ( bday ` n ) <-> ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) )
46 42 45 sylib 
 |-  ( n e. NN0_s -> ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) )
47 peano2 
 |-  ( ( bday ` n ) e. _om -> suc ( bday ` n ) e. _om )
48 peano2 
 |-  ( suc ( bday ` n ) e. _om -> suc suc ( bday ` n ) e. _om )
49 47 48 syl 
 |-  ( ( bday ` n ) e. _om -> suc suc ( bday ` n ) e. _om )
50 elnn 
 |-  ( ( ( bday ` ( n +s 1s ) ) e. suc suc ( bday ` n ) /\ suc suc ( bday ` n ) e. _om ) -> ( bday ` ( n +s 1s ) ) e. _om )
51 46 49 50 syl2an 
 |-  ( ( n e. NN0_s /\ ( bday ` n ) e. _om ) -> ( bday ` ( n +s 1s ) ) e. _om )
52 51 ex 
 |-  ( n e. NN0_s -> ( ( bday ` n ) e. _om -> ( bday ` ( n +s 1s ) ) e. _om ) )
53 2 4 6 8 11 52 n0sind 
 |-  ( A e. NN0_s -> ( bday ` A ) e. _om )