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

Proof

Step Hyp Ref Expression
1 etasslt2 A s B x No A s x x s B bday x suc bday A B
2 scutbday A s B bday A | s B = bday y No | A s y y s B
3 2 adantr A s B x No A s x x s B bday x suc bday A B bday A | s B = bday y No | A s y y s B
4 bdayfn bday Fn No
5 ssrab2 y No | A s y y s B No
6 simprl A s B x No A s x x s B bday x suc bday A B x No
7 simprr1 A s B x No A s x x s B bday x suc bday A B A s x
8 simprr2 A s B x No A s x x s B bday x suc bday A B x s B
9 7 8 jca A s B x No A s x x s B bday x suc bday A B A s x x s B
10 sneq y = x y = x
11 10 breq2d y = x A s y A s x
12 10 breq1d y = x y s B x s B
13 11 12 anbi12d y = x A s y y s B A s x x s B
14 13 elrab x y No | A s y y s B x No A s x x s B
15 6 9 14 sylanbrc A s B x No A s x x s B bday x suc bday A B x y No | A s y y s B
16 fnfvima bday Fn No y No | A s y y s B No x y No | A s y y s B bday x bday y No | A s y y s B
17 4 5 15 16 mp3an12i A s B x No A s x x s B bday x suc bday A B bday x bday y No | A s y y s B
18 intss1 bday x bday y No | A s y y s B bday y No | A s y y s B bday x
19 17 18 syl A s B x No A s x x s B bday x suc bday A B bday y No | A s y y s B bday x
20 3 19 eqsstrd A s B x No A s x x s B bday x suc bday A B bday A | s B bday x
21 simprr3 A s B x No A s x x s B bday x suc bday A B bday x suc bday A B
22 20 21 sstrd A s B x No A s x x s B bday x suc bday A B bday A | s B suc bday A B
23 22 rexlimdvaa A s B x No A s x x s B bday x suc bday A B bday A | s B suc bday A B
24 1 23 mpd A s B bday A | s B suc bday A B