Metamath Proof Explorer


Theorem scutbday

Description: The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion scutbday A s B bday A | s B = bday x No | A s x x s B

Proof

Step Hyp Ref Expression
1 scutval A s B A | s B = ι y x No | A s x x s B | bday y = bday x No | A s x x s B
2 1 eqcomd A s B ι y x No | A s x x s B | bday y = bday x No | A s x x s B = A | s B
3 scutcut A s B A | s B No A s A | s B A | s B s B
4 sneq x = A | s B x = A | s B
5 4 breq2d x = A | s B A s x A s A | s B
6 4 breq1d x = A | s B x s B A | s B s B
7 5 6 anbi12d x = A | s B A s x x s B A s A | s B A | s B s B
8 7 elrab A | s B x No | A s x x s B A | s B No A s A | s B A | s B s B
9 3anass A | s B No A s A | s B A | s B s B A | s B No A s A | s B A | s B s B
10 8 9 bitr4i A | s B x No | A s x x s B A | s B No A s A | s B A | s B s B
11 3 10 sylibr A s B A | s B x No | A s x x s B
12 conway A s B ∃! y x No | A s x x s B bday y = bday x No | A s x x s B
13 fveqeq2 y = A | s B bday y = bday x No | A s x x s B bday A | s B = bday x No | A s x x s B
14 13 riota2 A | s B x No | A s x x s B ∃! y x No | A s x x s B bday y = bday x No | A s x x s B bday A | s B = bday x No | A s x x s B ι y x No | A s x x s B | bday y = bday x No | A s x x s B = A | s B
15 11 12 14 syl2anc A s B bday A | s B = bday x No | A s x x s B ι y x No | A s x x s B | bday y = bday x No | A s x x s B = A | s B
16 2 15 mpbird A s B bday A | s B = bday x No | A s x x s B