Metamath Proof Explorer

Theorem scutbdaybnd2lim

Description: An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 scutbdaybnd2 
 |-  ( A < ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) )
2 1 adantr 
 |-  ( ( A < ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) )
3 bdayfun 
 |-  Fun bday
4 ssltex1 
 |-  ( A < A e. _V )
5 ssltex2 
 |-  ( A < B e. _V )
6 unexg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
7 4 5 6 syl2anc 
 |-  ( A < ( A u. B ) e. _V )
8 funimaexg 
 |-  ( ( Fun bday /\ ( A u. B ) e. _V ) -> ( bday " ( A u. B ) ) e. _V )
9 3 7 8 sylancr 
 |-  ( A < ( bday " ( A u. B ) ) e. _V )
10 9 uniexd 
 |-  ( A < U. ( bday " ( A u. B ) ) e. _V )
11 10 adantr 
 |-  ( ( A < U. ( bday " ( A u. B ) ) e. _V )
12 nlimsucg 
 |-  ( U. ( bday " ( A u. B ) ) e. _V -> -. Lim suc U. ( bday " ( A u. B ) ) )
13 11 12 syl 
 |-  ( ( A < -. Lim suc U. ( bday " ( A u. B ) ) )
14 limeq 
 |-  ( ( bday ` ( A |s B ) ) = suc U. ( bday " ( A u. B ) ) -> ( Lim ( bday ` ( A |s B ) ) <-> Lim suc U. ( bday " ( A u. B ) ) ) )
15 14 biimpcd 
 |-  ( Lim ( bday ` ( A |s B ) ) -> ( ( bday ` ( A |s B ) ) = suc U. ( bday " ( A u. B ) ) -> Lim suc U. ( bday " ( A u. B ) ) ) )
16 15 adantl 
 |-  ( ( A < ( ( bday ` ( A |s B ) ) = suc U. ( bday " ( A u. B ) ) -> Lim suc U. ( bday " ( A u. B ) ) ) )
17 13 16 mtod 
 |-  ( ( A < -. ( bday ` ( A |s B ) ) = suc U. ( bday " ( A u. B ) ) )
18 17 neqned 
 |-  ( ( A < ( bday ` ( A |s B ) ) =/= suc U. ( bday " ( A u. B ) ) )
19 bdayelon 
 |-  ( bday ` ( A |s B ) ) e. On
20 19 onordi 
 |-  Ord ( bday ` ( A |s B ) )
21 imassrn 
 |-  ( bday " ( A u. B ) ) C_ ran bday
22 bdayrn 
 |-  ran bday = On
23 21 22 sseqtri 
 |-  ( bday " ( A u. B ) ) C_ On
24 ssorduni 
 |-  ( ( bday " ( A u. B ) ) C_ On -> Ord U. ( bday " ( A u. B ) ) )
25 23 24 ax-mp 
 |-  Ord U. ( bday " ( A u. B ) )
26 ordsuc 
 |-  ( Ord U. ( bday " ( A u. B ) ) <-> Ord suc U. ( bday " ( A u. B ) ) )
27 25 26 mpbi 
 |-  Ord suc U. ( bday " ( A u. B ) )
28 ordelssne 
 |-  ( ( Ord ( bday ` ( A |s B ) ) /\ Ord suc U. ( bday " ( A u. B ) ) ) -> ( ( bday ` ( A |s B ) ) e. suc U. ( bday " ( A u. B ) ) <-> ( ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) /\ ( bday ` ( A |s B ) ) =/= suc U. ( bday " ( A u. B ) ) ) ) )
29 20 27 28 mp2an 
 |-  ( ( bday ` ( A |s B ) ) e. suc U. ( bday " ( A u. B ) ) <-> ( ( bday ` ( A |s B ) ) C_ suc U. ( bday " ( A u. B ) ) /\ ( bday ` ( A |s B ) ) =/= suc U. ( bday " ( A u. B ) ) ) )
30 2 18 29 sylanbrc 
 |-  ( ( A < ( bday ` ( A |s B ) ) e. suc U. ( bday " ( A u. B ) ) )
31 19 a1i 
 |-  ( ( A < ( bday ` ( A |s B ) ) e. On )
32 ordsssuc 
 |-  ( ( ( bday ` ( A |s B ) ) e. On /\ Ord U. ( bday " ( A u. B ) ) ) -> ( ( bday ` ( A |s B ) ) C_ U. ( bday " ( A u. B ) ) <-> ( bday ` ( A |s B ) ) e. suc U. ( bday " ( A u. B ) ) ) )
33 31 25 32 sylancl 
 |-  ( ( A < ( ( bday ` ( A |s B ) ) C_ U. ( bday " ( A u. B ) ) <-> ( bday ` ( A |s B ) ) e. suc U. ( bday " ( A u. B ) ) ) )
34 30 33 mpbird 
 |-  ( ( A < ( bday ` ( A |s B ) ) C_ U. ( bday " ( A u. B ) ) )