Metamath Proof Explorer


Theorem bday1s

Description: The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion bday1s
|- ( bday ` 1s ) = 1o

Proof

Step Hyp Ref Expression
1 df-1s
 |-  1s = ( { 0s } |s (/) )
2 1 fveq2i
 |-  ( bday ` 1s ) = ( bday ` ( { 0s } |s (/) ) )
3 0sno
 |-  0s e. No
4 snelpwi
 |-  ( 0s e. No -> { 0s } e. ~P No )
5 3 4 ax-mp
 |-  { 0s } e. ~P No
6 nulssgt
 |-  ( { 0s } e. ~P No -> { 0s } <
7 5 6 ax-mp
 |-  { 0s } <
8 scutbdaybnd2
 |-  ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) )
9 7 8 ax-mp
 |-  ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) )
10 un0
 |-  ( { 0s } u. (/) ) = { 0s }
11 10 imaeq2i
 |-  ( bday " ( { 0s } u. (/) ) ) = ( bday " { 0s } )
12 bdayfn
 |-  bday Fn No
13 fnsnfv
 |-  ( ( bday Fn No /\ 0s e. No ) -> { ( bday ` 0s ) } = ( bday " { 0s } ) )
14 12 3 13 mp2an
 |-  { ( bday ` 0s ) } = ( bday " { 0s } )
15 bday0s
 |-  ( bday ` 0s ) = (/)
16 15 sneqi
 |-  { ( bday ` 0s ) } = { (/) }
17 11 14 16 3eqtr2i
 |-  ( bday " ( { 0s } u. (/) ) ) = { (/) }
18 17 unieqi
 |-  U. ( bday " ( { 0s } u. (/) ) ) = U. { (/) }
19 0ex
 |-  (/) e. _V
20 19 unisn
 |-  U. { (/) } = (/)
21 18 20 eqtri
 |-  U. ( bday " ( { 0s } u. (/) ) ) = (/)
22 suceq
 |-  ( U. ( bday " ( { 0s } u. (/) ) ) = (/) -> suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) )
23 21 22 ax-mp
 |-  suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/)
24 df-1o
 |-  1o = suc (/)
25 23 24 eqtr4i
 |-  suc U. ( bday " ( { 0s } u. (/) ) ) = 1o
26 9 25 sseqtri
 |-  ( bday ` ( { 0s } |s (/) ) ) C_ 1o
27 ssrab2
 |-  { x e. No | ( { 0s } <
28 fnssintima
 |-  ( ( bday Fn No /\ { x e. No | ( { 0s } < ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } <
29 12 27 28 mp2an
 |-  ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } <
30 sneq
 |-  ( x = y -> { x } = { y } )
31 30 breq2d
 |-  ( x = y -> ( { 0s } < { 0s } <
32 30 breq1d
 |-  ( x = y -> ( { x } < { y } <
33 31 32 anbi12d
 |-  ( x = y -> ( ( { 0s } < ( { 0s } <
34 33 elrab
 |-  ( y e. { x e. No | ( { 0s } < ( y e. No /\ ( { 0s } <
35 sltirr
 |-  ( 0s e. No -> -. 0s 
36 3 35 ax-mp
 |-  -. 0s 
37 breq2
 |-  ( y = 0s -> ( 0s  0s 
38 36 37 mtbiri
 |-  ( y = 0s -> -. 0s 
39 38 necon2ai
 |-  ( 0s  y =/= 0s )
40 bday0b
 |-  ( y e. No -> ( ( bday ` y ) = (/) <-> y = 0s ) )
41 40 necon3bid
 |-  ( y e. No -> ( ( bday ` y ) =/= (/) <-> y =/= 0s ) )
42 39 41 syl5ibr
 |-  ( y e. No -> ( 0s  ( bday ` y ) =/= (/) ) )
43 bdayelon
 |-  ( bday ` y ) e. On
44 43 onordi
 |-  Ord ( bday ` y )
45 ordge1n0
 |-  ( Ord ( bday ` y ) -> ( 1o C_ ( bday ` y ) <-> ( bday ` y ) =/= (/) ) )
46 44 45 ax-mp
 |-  ( 1o C_ ( bday ` y ) <-> ( bday ` y ) =/= (/) )
47 42 46 syl6ibr
 |-  ( y e. No -> ( 0s  1o C_ ( bday ` y ) ) )
48 ssltsep
 |-  ( { 0s } < A. x e. { 0s } A. z e. { y } x 
49 vex
 |-  y e. _V
50 breq2
 |-  ( z = y -> ( x  x 
51 49 50 ralsn
 |-  ( A. z e. { y } x  x 
52 51 ralbii
 |-  ( A. x e. { 0s } A. z e. { y } x  A. x e. { 0s } x 
53 3 elexi
 |-  0s e. _V
54 breq1
 |-  ( x = 0s -> ( x  0s 
55 53 54 ralsn
 |-  ( A. x e. { 0s } x  0s 
56 52 55 bitri
 |-  ( A. x e. { 0s } A. z e. { y } x  0s 
57 48 56 sylib
 |-  ( { 0s } < 0s 
58 47 57 impel
 |-  ( ( y e. No /\ { 0s } < 1o C_ ( bday ` y ) )
59 58 adantrr
 |-  ( ( y e. No /\ ( { 0s } < 1o C_ ( bday ` y ) )
60 34 59 sylbi
 |-  ( y e. { x e. No | ( { 0s } < 1o C_ ( bday ` y ) )
61 29 60 mprgbir
 |-  1o C_ |^| ( bday " { x e. No | ( { 0s } <
62 scutbday
 |-  ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } <
63 7 62 ax-mp
 |-  ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } <
64 61 63 sseqtrri
 |-  1o C_ ( bday ` ( { 0s } |s (/) ) )
65 26 64 eqssi
 |-  ( bday ` ( { 0s } |s (/) ) ) = 1o
66 2 65 eqtri
 |-  ( bday ` 1s ) = 1o