Metamath Proof Explorer


Theorem scutval

Description: The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion scutval A s B A | s B = ι x y No | A s y y s B | bday x = bday y No | A s y y s B

Proof

Step Hyp Ref Expression
1 ssltex1 A s B A V
2 ssltss1 A s B A No
3 1 2 elpwd A s B A 𝒫 No
4 df-br A s B A B s
5 4 biimpi A s B A B s
6 ssltex2 A s B B V
7 elimasng A V B V B s A A B s
8 1 6 7 syl2anc A s B B s A A B s
9 5 8 mpbird A s B B s A
10 riotaex ι x y No | A s y y s B | bday x = bday y No | A s y y s B V
11 breq1 a = A a s y A s y
12 breq2 b = B y s b y s B
13 11 12 bi2anan9 a = A b = B a s y y s b A s y y s B
14 13 rabbidv a = A b = B y No | a s y y s b = y No | A s y y s B
15 14 imaeq2d a = A b = B bday y No | a s y y s b = bday y No | A s y y s B
16 15 inteqd a = A b = B bday y No | a s y y s b = bday y No | A s y y s B
17 16 eqeq2d a = A b = B bday x = bday y No | a s y y s b bday x = bday y No | A s y y s B
18 14 17 riotaeqbidv a = A b = B ι x y No | a s y y s b | bday x = bday y No | a s y y s b = ι x y No | A s y y s B | bday x = bday y No | A s y y s B
19 sneq a = A a = A
20 19 imaeq2d a = A s a = s A
21 df-scut | s = a 𝒫 No , b s a ι x y No | a s y y s b | bday x = bday y No | a s y y s b
22 18 20 21 ovmpox A 𝒫 No B s A ι x y No | A s y y s B | bday x = bday y No | A s y y s B V A | s B = ι x y No | A s y y s B | bday x = bday y No | A s y y s B
23 10 22 mp3an3 A 𝒫 No B s A A | s B = ι x y No | A s y y s B | bday x = bday y No | A s y y s B
24 3 9 23 syl2anc A s B A | s B = ι x y No | A s y y s B | bday x = bday y No | A s y y s B