Theorem cuteq1

Description: Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cuteq1.1	|- ( ph -> 0s e. A )
2		cuteq1.2	|- ( ph -> A <
3		cuteq1.3	|- ( ph -> { 1s } <
4		bday1s	|- ( bday ` 1s ) = 1o
5		df-1o	|- 1o = suc (/)
6	4 5	eqtri	|- ( bday ` 1s ) = suc (/)
7		ssltsep	|- ( A < A. x e. A A. y e. { 0s } x
8		dfral2	|- ( A. y e. { 0s } x -. E. y e. { 0s } -. x
9	8	ralbii	|- ( A. x e. A A. y e. { 0s } x A. x e. A -. E. y e. { 0s } -. x
10		ralnex	|- ( A. x e. A -. E. y e. { 0s } -. x -. E. x e. A E. y e. { 0s } -. x
11	9 10	bitri	|- ( A. x e. A A. y e. { 0s } x -. E. x e. A E. y e. { 0s } -. x
12	7 11	sylib	|- ( A < -. E. x e. A E. y e. { 0s } -. x
13		0sno	|- 0s e. No
14		sltirr	|- ( 0s e. No -> -. 0s
15	13 14	ax-mp	|- -. 0s
16		breq1	|- ( x = 0s -> ( x 0s
17	16	notbid	|- ( x = 0s -> ( -. x -. 0s
18	17	rspcev	|- ( ( 0s e. A /\ -. 0s E. x e. A -. x
19	1 15 18	sylancl	|- ( ph -> E. x e. A -. x
20	13	elexi	|- 0s e. _V
21		breq2	|- ( y = 0s -> ( x x
22	21	notbid	|- ( y = 0s -> ( -. x -. x
23	20 22	rexsn	|- ( E. y e. { 0s } -. x -. x
24	23	rexbii	|- ( E. x e. A E. y e. { 0s } -. x E. x e. A -. x
25	19 24	sylibr	|- ( ph -> E. x e. A E. y e. { 0s } -. x
26	12 25	nsyl3	|- ( ph -> -. A <
27	26	adantr	|- ( ( ph /\ x e. No ) -> -. A <
28		sneq	|- ( x = 0s -> { x } = { 0s } )
29	28	breq2d	|- ( x = 0s -> ( A < A <
30	29	notbid	|- ( x = 0s -> ( -. A < -. A <
31	27 30	syl5ibrcom	|- ( ( ph /\ x e. No ) -> ( x = 0s -> -. A <
32	31	necon2ad	|- ( ( ph /\ x e. No ) -> ( A < x =/= 0s ) )
33	32	adantrd	|- ( ( ph /\ x e. No ) -> ( ( A < x =/= 0s ) )
34	33	impr	|- ( ( ph /\ ( x e. No /\ ( A < x =/= 0s )
35		bday0b	|- ( x e. No -> ( ( bday ` x ) = (/) <-> x = 0s ) )
36	35	ad2antrl	|- ( ( ph /\ ( x e. No /\ ( A < ( ( bday ` x ) = (/) <-> x = 0s ) )
37	36	necon3bid	|- ( ( ph /\ ( x e. No /\ ( A < ( ( bday ` x ) =/= (/) <-> x =/= 0s ) )
38	34 37	mpbird	|- ( ( ph /\ ( x e. No /\ ( A < ( bday ` x ) =/= (/) )
39		bdayelon	|- ( bday ` x ) e. On
40	39	onordi	|- Ord ( bday ` x )
41		ord0eln0	|- ( Ord ( bday ` x ) -> ( (/) e. ( bday ` x ) <-> ( bday ` x ) =/= (/) ) )
42	40 41	ax-mp	|- ( (/) e. ( bday ` x ) <-> ( bday ` x ) =/= (/) )
43		0elon	|- (/) e. On
44	43 39	onsucssi	|- ( (/) e. ( bday ` x ) <-> suc (/) C_ ( bday ` x ) )
45	42 44	bitr3i	|- ( ( bday ` x ) =/= (/) <-> suc (/) C_ ( bday ` x ) )
46	38 45	sylib	|- ( ( ph /\ ( x e. No /\ ( A < suc (/) C_ ( bday ` x ) )
47	6 46	eqsstrid	|- ( ( ph /\ ( x e. No /\ ( A < ( bday ` 1s ) C_ ( bday ` x ) )
48	47	expr	|- ( ( ph /\ x e. No ) -> ( ( A < ( bday ` 1s ) C_ ( bday ` x ) ) )
49	48	ralrimiva	|- ( ph -> A. x e. No ( ( A < ( bday ` 1s ) C_ ( bday ` x ) ) )
50		1sno	|- 1s e. No
51	50	elexi	|- 1s e. _V
52	51	snnz	|- { 1s } =/= (/)
53		sslttr	|- ( ( A < A <
54	52 53	mp3an3	|- ( ( A < A <
55	2 3 54	syl2anc	|- ( ph -> A <
56		eqscut2	|- ( ( A < ( ( A |s B ) = 1s <-> ( A < ( bday ` 1s ) C_ ( bday ` x ) ) ) ) )
57	55 50 56	sylancl	|- ( ph -> ( ( A |s B ) = 1s <-> ( A < ( bday ` 1s ) C_ ( bday ` x ) ) ) ) )
58	2 3 49 57	mpbir3and	|- ( ph -> ( A |s B ) = 1s )