Theorem cuteq0

Description: Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Hypotheses	cuteq0.1	|- ( ph -> A <
	cuteq0.2	|- ( ph -> { 0s } <
Assertion	cuteq0	|- ( ph -> ( A |s B ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		cuteq0.1	|- ( ph -> A <
2		cuteq0.2	|- ( ph -> { 0s } <
3		bday0s	|- ( bday ` 0s ) = (/)
4	3	a1i	|- ( ph -> ( bday ` 0s ) = (/) )
5		0sno	|- 0s e. No
6		sneq	|- ( y = 0s -> { y } = { 0s } )
7	6	breq2d	|- ( y = 0s -> ( A < A <
8	6	breq1d	|- ( y = 0s -> ( { y } < { 0s } <
9	7 8	anbi12d	|- ( y = 0s -> ( ( A < ( A <
10		fveqeq2	|- ( y = 0s -> ( ( bday ` y ) = (/) <-> ( bday ` 0s ) = (/) ) )
11	9 10	anbi12d	|- ( y = 0s -> ( ( ( A < ( ( A <
12	11	rspcev	|- ( ( 0s e. No /\ ( ( A < E. y e. No ( ( A <
13	5 12	mpan	|- ( ( ( A < E. y e. No ( ( A <
14	1 2 4 13	syl21anc	|- ( ph -> E. y e. No ( ( A <
15		bdayfn	|- bday Fn No
16		ssrab2	|- { x e. No | ( A <
17		fvelimab	|- ( ( bday Fn No /\ { x e. No | ( A < ( (/) e. ( bday " { x e. No | ( A < E. y e. { x e. No | ( A <
18	15 16 17	mp2an	|- ( (/) e. ( bday " { x e. No | ( A < E. y e. { x e. No | ( A <
19		sneq	|- ( x = y -> { x } = { y } )
20	19	breq2d	|- ( x = y -> ( A < A <
21	19	breq1d	|- ( x = y -> ( { x } < { y } <
22	20 21	anbi12d	|- ( x = y -> ( ( A < ( A <
23	22	rexrab	|- ( E. y e. { x e. No | ( A < E. y e. No ( ( A <
24	18 23	bitri	|- ( (/) e. ( bday " { x e. No | ( A < E. y e. No ( ( A <
25	14 24	sylibr	|- ( ph -> (/) e. ( bday " { x e. No | ( A <
26		int0el	|- ( (/) e. ( bday " { x e. No | ( A < |^| ( bday " { x e. No | ( A <
27	25 26	syl	|- ( ph -> |^| ( bday " { x e. No | ( A <
28	3 27	eqtr4id	|- ( ph -> ( bday ` 0s ) = |^| ( bday " { x e. No | ( A <
29	5	elexi	|- 0s e. _V
30	29	snnz	|- { 0s } =/= (/)
31		sslttr	|- ( ( A < A <
32	30 31	mp3an3	|- ( ( A < A <
33	1 2 32	syl2anc	|- ( ph -> A <
34		eqscut	|- ( ( A < ( ( A |s B ) = 0s <-> ( A <
35	33 5 34	sylancl	|- ( ph -> ( ( A |s B ) = 0s <-> ( A <
36	1 2 28 35	mpbir3and	|- ( ph -> ( A |s B ) = 0s )