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