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 s B Lim bday A | s B bday A | s B bday A B

Proof

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