Metamath Proof Explorer


Theorem scutbdaybnd

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

Ref Expression
Assertion scutbdaybnd A s B O On bday A B O bday A | s B O

Proof

Step Hyp Ref Expression
1 etasslt A s B O On bday A B O x No A s x x s B bday x O
2 simpl1 A s B O On bday A B O x No A s x x s B bday x O A s B
3 scutbday A s B bday A | s B = bday y No | A s y y s B
4 2 3 syl A s B O On bday A B O x No A s x x s B bday x O bday A | s B = bday y No | A s y y s B
5 bdayfn bday Fn No
6 ssrab2 y No | A s y y s B No
7 sneq y = x y = x
8 7 breq2d y = x A s y A s x
9 7 breq1d y = x y s B x s B
10 8 9 anbi12d y = x A s y y s B A s x x s B
11 simprl A s B O On bday A B O x No A s x x s B bday x O x No
12 simprr1 A s B O On bday A B O x No A s x x s B bday x O A s x
13 simprr2 A s B O On bday A B O x No A s x x s B bday x O x s B
14 12 13 jca A s B O On bday A B O x No A s x x s B bday x O A s x x s B
15 10 11 14 elrabd A s B O On bday A B O x No A s x x s B bday x O 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 5 6 15 16 mp3an12i A s B O On bday A B O x No A s x x s B bday x O 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 O On bday A B O x No A s x x s B bday x O bday y No | A s y y s B bday x
20 4 19 eqsstrd A s B O On bday A B O x No A s x x s B bday x O bday A | s B bday x
21 simprr3 A s B O On bday A B O x No A s x x s B bday x O bday x O
22 20 21 sstrd A s B O On bday A B O x No A s x x s B bday x O bday A | s B O
23 1 22 rexlimddv A s B O On bday A B O bday A | s B O