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 < ( bday ` ( A |s B ) ) = |^| ( bday " { x e. No | ( A <

Proof

Step	Hyp	Ref	Expression
1		scutval	|- ( A < ( A |s B ) = ( iota_ y e. { x e. No | ( A <
2	1	eqcomd	|- ( A < ( iota_ y e. { x e. No | ( A <
3		scutcut	|- ( A < ( ( A |s B ) e. No /\ A <
4		sneq	|- ( x = ( A |s B ) -> { x } = { ( A |s B ) } )
5	4	breq2d	|- ( x = ( A |s B ) -> ( A < A <
6	4	breq1d	|- ( x = ( A |s B ) -> ( { x } < { ( A |s B ) } <
7	5 6	anbi12d	|- ( x = ( A |s B ) -> ( ( A < ( A <
8	7	elrab	|- ( ( A |s B ) e. { x e. No | ( A < ( ( A |s B ) e. No /\ ( A <
9		3anass	|- ( ( ( A |s B ) e. No /\ A < ( ( A |s B ) e. No /\ ( A <
10	8 9	bitr4i	|- ( ( A |s B ) e. { x e. No | ( A < ( ( A |s B ) e. No /\ A <
11	3 10	sylibr	|- ( A < ( A |s B ) e. { x e. No | ( A <
12		conway	|- ( A < E! y e. { x e. No | ( A <
13		fveqeq2	|- ( y = ( A |s B ) -> ( ( bday ` y ) = |^| ( bday " { x e. No | ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { x e. No | ( A <
14	13	riota2	|- ( ( ( A |s B ) e. { x e. No | ( A < ( ( bday ` ( A |s B ) ) = |^| ( bday " { x e. No | ( A < ( iota_ y e. { x e. No | ( A <
15	11 12 14	syl2anc	|- ( A < ( ( bday ` ( A |s B ) ) = |^| ( bday " { x e. No | ( A < ( iota_ y e. { x e. No | ( A <
16	2 15	mpbird	|- ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { x e. No | ( A <