Theorem n0scut

Description: A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025)

	Ref	Expression
Assertion	n0scut	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢y=0_s\to y=0_s$$
2		oveq1	$$⊢y=0_s\to y{-}_s{1}_s=0_s{-}_s{1}_s$$
3	2	sneqd	$$⊢y=0_s\to \left\{y{-}_s{1}_s\right\}=\left\{0_s{-}_s{1}_s\right\}$$
4	3	oveq1d	$$⊢y=0_s\to \left\{y{-}_s{1}_s\right\}{|}_s\varnothing =\left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing$$
5	1 4	eqeq12d	$$⊢y=0_s\to \left(y=\left\{y{-}_s{1}_s\right\}{|}_s\varnothing \leftrightarrow 0_s=\left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing \right)$$
6		id	$$⊢y=x\to y=x$$
7		oveq1	$$⊢y=x\to y{-}_s{1}_s=x{-}_s{1}_s$$
8	7	sneqd	$$⊢y=x\to \left\{y{-}_s{1}_s\right\}=\left\{x{-}_s{1}_s\right\}$$
9	8	oveq1d	$$⊢y=x\to \left\{y{-}_s{1}_s\right\}{|}_s\varnothing =\left\{x{-}_s{1}_s\right\}{|}_s\varnothing$$
10	6 9	eqeq12d	$$⊢y=x\to \left(y=\left\{y{-}_s{1}_s\right\}{|}_s\varnothing \leftrightarrow x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)$$
11		id	$$⊢y=x{+}_s{1}_s\to y=x{+}_s{1}_s$$
12		oveq1	$$⊢y=x{+}_s{1}_s\to y{-}_s{1}_s=\left(x{+}_s{1}_s\right){-}_s{1}_s$$
13	12	sneqd	$$⊢y=x{+}_s{1}_s\to \left\{y{-}_s{1}_s\right\}=\left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}$$
14	13	oveq1d	$$⊢y=x{+}_s{1}_s\to \left\{y{-}_s{1}_s\right\}{|}_s\varnothing =\left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing$$
15	11 14	eqeq12d	$$⊢y=x{+}_s{1}_s\to \left(y=\left\{y{-}_s{1}_s\right\}{|}_s\varnothing \leftrightarrow x{+}_s{1}_s=\left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing \right)$$
16		id	$$⊢y=A\to y=A$$
17		oveq1	$$⊢y=A\to y{-}_s{1}_s=A{-}_s{1}_s$$
18	17	sneqd	$$⊢y=A\to \left\{y{-}_s{1}_s\right\}=\left\{A{-}_s{1}_s\right\}$$
19	18	oveq1d	$$⊢y=A\to \left\{y{-}_s{1}_s\right\}{|}_s\varnothing =\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$
20	16 19	eqeq12d	$$⊢y=A\to \left(y=\left\{y{-}_s{1}_s\right\}{|}_s\varnothing \leftrightarrow A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing \right)$$
21		0sno	$$⊢0_s\in \mathrm{No}$$
22		1sno	$$⊢1_s\in \mathrm{No}$$
23		subscl	$$⊢\left(0_s\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to 0_s{-}_s{1}_s\in \mathrm{No}$$
24	21 22 23	mp2an	$$⊢0_s{-}_s{1}_s\in \mathrm{No}$$
25	24	a1i	$$⊢\top \to 0_s{-}_s{1}_s\in \mathrm{No}$$
26	21	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
27	26	sltm1d	$$⊢\top \to \left(0_s{-}_s{1}_s\right){<}_s{0}_s$$
28	25 27	cutneg	$$⊢\top \to \left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing =0_s$$
29	28	mptru	$$⊢\left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing =0_s$$
30	29	eqcomi	$$⊢0_s=\left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing$$
31		ovex	$$⊢x{-}_s{1}_s\in \mathrm{V}$$
32		oveq1	$$⊢b=x{-}_s{1}_s\to b{+}_s{1}_s=\left(x{-}_s{1}_s\right){+}_s{1}_s$$
33	32	eqeq2d	$$⊢b=x{-}_s{1}_s\to \left(a=b{+}_s{1}_s\leftrightarrow a=\left(x{-}_s{1}_s\right){+}_s{1}_s\right)$$
34	31 33	rexsn	$$⊢\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\leftrightarrow a=\left(x{-}_s{1}_s\right){+}_s{1}_s$$
35		n0sno	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in \mathrm{No}$$
36		npcans	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(x{-}_s{1}_s\right){+}_s{1}_s=x$$
37	35 22 36	sylancl	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left(x{-}_s{1}_s\right){+}_s{1}_s=x$$
38	37	adantr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(x{-}_s{1}_s\right){+}_s{1}_s=x$$
39	38	eqeq2d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(a=\left(x{-}_s{1}_s\right){+}_s{1}_s\leftrightarrow a=x\right)$$
40	34 39	bitrid	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\leftrightarrow a=x\right)$$
41	40	alrimiv	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \forall a\left(\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\leftrightarrow a=x\right)$$
42		absn	$$⊢\left\{a|\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\right\}=\left\{x\right\}\leftrightarrow \forall a\left(\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\leftrightarrow a=x\right)$$
43	41 42	sylibr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{a|\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\right\}=\left\{x\right\}$$
44	21	elexi	$$⊢0_s\in \mathrm{V}$$
45		oveq2	$$⊢b=0_s\to x{+}_{s}b=x{+}_s{0}_s$$
46	45	eqeq2d	$$⊢b=0_s\to \left(a=x{+}_{s}b\leftrightarrow a=x{+}_s{0}_s\right)$$
47	44 46	rexsn	$$⊢\exists b\in \left\{0_s\right\}a=x{+}_{s}b\leftrightarrow a=x{+}_s{0}_s$$
48	35	addsridd	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x{+}_s{0}_s=x$$
49	48	adantr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x{+}_s{0}_s=x$$
50	49	eqeq2d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(a=x{+}_s{0}_s\leftrightarrow a=x\right)$$
51	47 50	bitrid	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(\exists b\in \left\{0_s\right\}a=x{+}_{s}b\leftrightarrow a=x\right)$$
52	51	alrimiv	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \forall a\left(\exists b\in \left\{0_s\right\}a=x{+}_{s}b\leftrightarrow a=x\right)$$
53		absn	$$⊢\left\{a|\exists b\in \left\{0_s\right\}a=x{+}_{s}b\right\}=\left\{x\right\}\leftrightarrow \forall a\left(\exists b\in \left\{0_s\right\}a=x{+}_{s}b\leftrightarrow a=x\right)$$
54	52 53	sylibr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{a|\exists b\in \left\{0_s\right\}a=x{+}_{s}b\right\}=\left\{x\right\}$$
55	43 54	uneq12d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{a|\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \left\{0_s\right\}a=x{+}_{s}b\right\}=\left\{x\right\}\cup \left\{x\right\}$$
56		unidm	$$⊢\left\{x\right\}\cup \left\{x\right\}=\left\{x\right\}$$
57	55 56	eqtrdi	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{a|\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \left\{0_s\right\}a=x{+}_{s}b\right\}=\left\{x\right\}$$
58		rex0	$$⊢\neg \exists b\in \varnothing a=b{+}_s{1}_s$$
59	58	abf	$$⊢\left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}=\varnothing$$
60		rex0	$$⊢\neg \exists b\in \varnothing a=x{+}_{s}b$$
61	60	abf	$$⊢\left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}=\varnothing$$
62	59 61	uneq12i	$$⊢\left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}=\varnothing \cup \varnothing$$
63		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
64	62 63	eqtri	$$⊢\left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}=\varnothing$$
65	64	a1i	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}=\varnothing$$
66	57 65	oveq12d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(\left\{a|\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \left\{0_s\right\}a=x{+}_{s}b\right\}\right){|}_s\left(\left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}\right)=\left\{x\right\}{|}_s\varnothing$$
67		subscl	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to x{-}_s{1}_s\in \mathrm{No}$$
68	35 22 67	sylancl	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x{-}_s{1}_s\in \mathrm{No}$$
69	68	adantr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x{-}_s{1}_s\in \mathrm{No}$$
70	31	snelpw	$$⊢x{-}_s{1}_s\in \mathrm{No}\leftrightarrow \left\{x{-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
71	69 70	sylib	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{x{-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
72		nulssgt	$$⊢\left\{x{-}_s{1}_s\right\}\in 𝒫\mathrm{No}\to \left\{x{-}_s{1}_s\right\}{\ll }_s\varnothing$$
73	71 72	syl	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{x{-}_s{1}_s\right\}{\ll }_s\varnothing$$
74	44	snelpw	$$⊢0_s\in \mathrm{No}\leftrightarrow \left\{0_s\right\}\in 𝒫\mathrm{No}$$
75	21 74	mpbi	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
76		nulssgt	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
77	75 76	mp1i	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{0_s\right\}{\ll }_s\varnothing$$
78		simpr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing$$
79		df-1s	$$⊢1_s=\left\{0_s\right\}{|}_s\varnothing$$
80	79	a1i	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to 1_s=\left\{0_s\right\}{|}_s\varnothing$$
81	73 77 78 80	addsunif	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x{+}_s{1}_s=\left(\left\{a|\exists b\in \left\{x{-}_s{1}_s\right\}a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \left\{0_s\right\}a=x{+}_{s}b\right\}\right){|}_s\left(\left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}\cup \left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}\right)$$
82	35	adantr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x\in \mathrm{No}$$
83		pncans	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(x{+}_s{1}_s\right){-}_s{1}_s=x$$
84	82 22 83	sylancl	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left(x{+}_s{1}_s\right){-}_s{1}_s=x$$
85	84	sneqd	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}=\left\{x\right\}$$
86	85	oveq1d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing =\left\{x\right\}{|}_s\varnothing$$
87	66 81 86	3eqtr4d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x{+}_s{1}_s=\left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing$$
88	87	ex	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left(x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \to x{+}_s{1}_s=\left\{\left(x{+}_s{1}_s\right){-}_s{1}_s\right\}{|}_s\varnothing \right)$$
89	5 10 15 20 30 88	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$