Theorem scutcut

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

	Ref	Expression
Assertion	scutcut	|- ( A < ( ( A |s B ) e. No /\ A <

Proof

Step	Hyp	Ref	Expression
1		scutval	|- ( A < ( A |s B ) = ( iota_ x e. { y e. No | ( A <
2		conway	|- ( A < E! x e. { y e. No | ( A <
3		riotacl	|- ( E! x e. { y e. No | ( A < ( iota_ x e. { y e. No | ( A <
4	2 3	syl	|- ( A < ( iota_ x e. { y e. No | ( A <
5	1 4	eqeltrd	|- ( A < ( A |s B ) e. { y e. No | ( A <
6		sneq	|- ( y = ( A |s B ) -> { y } = { ( A |s B ) } )
7	6	breq2d	|- ( y = ( A |s B ) -> ( A < A <
8	6	breq1d	|- ( y = ( A |s B ) -> ( { y } < { ( A |s B ) } <
9	7 8	anbi12d	|- ( y = ( A |s B ) -> ( ( A < ( A <
10	9	elrab	|- ( ( A |s B ) e. { y e. No | ( A < ( ( A |s B ) e. No /\ ( A <
11		3anass	|- ( ( ( A |s B ) e. No /\ A < ( ( A |s B ) e. No /\ ( A <
12	10 11	bitr4i	|- ( ( A |s B ) e. { y e. No | ( A < ( ( A |s B ) e. No /\ A <
13	5 12	sylib	|- ( A < ( ( A |s B ) e. No /\ A <