Theorem cuteq1

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

	Ref	Expression
Hypotheses	cuteq1.1	No typesetting found for |- ( ph -> 0s e. A ) with typecode |-
	cuteq1.2	No typesetting found for |- ( ph -> A <
	cuteq1.3	No typesetting found for |- ( ph -> { 1s } <
Assertion	cuteq1	Could not format assertion : No typesetting found for |- ( ph -> ( A |s B ) = 1s ) with typecode |-

Proof

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