Metamath Proof Explorer

Theorem scutbdaybnd2

Description: An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021)

Ref Expression
Assertion scutbdaybnd2 
|- ( A < ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 etasslt2 
 |-  ( A < E. x e. No ( A <
2 scutbday 
 |-  ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
3 2 adantr 
 |-  ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
4 bdayfn 
 |-  bday Fn No
5 ssrab2 
 |-  { y e. No | ( A <
6 simprl 
 |-  ( ( A < x e. No )
7 simprr1 
 |-  ( ( A < A <
8 simprr2 
 |-  ( ( A < { x } <
9 7 8 jca 
 |-  ( ( A < ( A <
10 sneq 
 |-  ( y = x -> { y } = { x } )
11 10 breq2d 
 |-  ( y = x -> ( A < A <
12 10 breq1d 
 |-  ( y = x -> ( { y } < { x } <
13 11 12 anbi12d 
 |-  ( y = x -> ( ( A < ( A <
14 13 elrab 
 |-  ( x e. { y e. No | ( A < ( x e. No /\ ( A <
15 6 9 14 sylanbrc 
 |-  ( ( A < x e. { y e. No | ( A <
16 fnfvima 
 |-  ( ( bday Fn No /\ { y e. No | ( A < ( bday ` x ) e. ( bday " { y e. No | ( A <
17 4 5 15 16 mp3an12i 
 |-  ( ( A < ( bday ` x ) e. ( bday " { y e. No | ( A <
18 intss1 
 |-  ( ( bday ` x ) e. ( bday " { y e. No | ( A < |^| ( bday " { y e. No | ( A <
19 17 18 syl 
 |-  ( ( A < |^| ( bday " { y e. No | ( A <
20 3 19 eqsstrd 
 |-  ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` x ) )
21 simprr3 
 |-  ( ( A < ( bday ` x ) C_ suc U. ( bday " ( A u. B ) ) )
22 20 21 sstrd 
 |-  ( ( A < ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) )
23 22 rexlimdvaa 
 |-  ( A < ( E. x e. No ( A < ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) ) )
24 1 23 mpd 
 |-  ( A < ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) )