Theorem n0scut

Description: A cut form for surreal naturals. (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		0slt1s	$$⊢0_s{<}_s{1}_s$$
28		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
29	22 28	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
30	27 29	breqtrri	$$⊢0_s{<}_s\left(0_s{+}_s{1}_s\right)$$
31	22	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
32	26 31 26	sltsubaddd	$$⊢\top \to \left(\left(0_s{-}_s{1}_s\right){<}_s{0}_s\leftrightarrow 0_s{<}_s\left(0_s{+}_s{1}_s\right)\right)$$
33	30 32	mpbiri	$$⊢\top \to \left(0_s{-}_s{1}_s\right){<}_s{0}_s$$
34	25 26 33	ssltsn	$$⊢\top \to \left\{0_s{-}_s{1}_s\right\}{\ll }_s\left\{0_s\right\}$$
35	21	elexi	$$⊢0_s\in \mathrm{V}$$
36	35	snelpw	$$⊢0_s\in \mathrm{No}\leftrightarrow \left\{0_s\right\}\in 𝒫\mathrm{No}$$
37	21 36	mpbi	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
38		nulssgt	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
39	37 38	ax-mp	$$⊢\left\{0_s\right\}{\ll }_s\varnothing$$
40	39	a1i	$$⊢\top \to \left\{0_s\right\}{\ll }_s\varnothing$$
41	34 40	cuteq0	$$⊢\top \to \left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing =0_s$$
42	41	mptru	$$⊢\left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing =0_s$$
43	42	eqcomi	$$⊢0_s=\left\{0_s{-}_s{1}_s\right\}{|}_s\varnothing$$
44		ovex	$$⊢x{-}_s{1}_s\in \mathrm{V}$$
45		oveq1	$$⊢b=x{-}_s{1}_s\to b{+}_s{1}_s=\left(x{-}_s{1}_s\right){+}_s{1}_s$$
46	45	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)$$
47	44 46	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$$
48		n0sno	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in \mathrm{No}$$
49		npcans	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(x{-}_s{1}_s\right){+}_s{1}_s=x$$
50	48 22 49	sylancl	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left(x{-}_s{1}_s\right){+}_s{1}_s=x$$
51	50	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$$
52	51	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)$$
53	47 52	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)$$
54	53	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)$$
55		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)$$
56	54 55	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\}$$
57		oveq2	$$⊢b=0_s\to x{+}_{s}b=x{+}_s{0}_s$$
58	57	eqeq2d	$$⊢b=0_s\to \left(a=x{+}_{s}b\leftrightarrow a=x{+}_s{0}_s\right)$$
59	35 58	rexsn	$$⊢\exists b\in \left\{0_s\right\}a=x{+}_{s}b\leftrightarrow a=x{+}_s{0}_s$$
60	48	addsridd	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x{+}_s{0}_s=x$$
61	60	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$$
62	61	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)$$
63	59 62	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)$$
64	63	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)$$
65		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)$$
66	64 65	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\}$$
67	56 66	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\}$$
68		unidm	$$⊢\left\{x\right\}\cup \left\{x\right\}=\left\{x\right\}$$
69	67 68	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\}$$
70		rex0	$$⊢\neg \exists b\in \varnothing a=b{+}_s{1}_s$$
71	70	abf	$$⊢\left\{a|\exists b\in \varnothing a=b{+}_s{1}_s\right\}=\varnothing$$
72		rex0	$$⊢\neg \exists b\in \varnothing a=x{+}_{s}b$$
73	72	abf	$$⊢\left\{a|\exists b\in \varnothing a=x{+}_{s}b\right\}=\varnothing$$
74	71 73	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$$
75		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
76	74 75	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$$
77	76	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$$
78	69 77	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$$
79		subscl	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to x{-}_s{1}_s\in \mathrm{No}$$
80	48 22 79	sylancl	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x{-}_s{1}_s\in \mathrm{No}$$
81	80	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}$$
82	44	snelpw	$$⊢x{-}_s{1}_s\in \mathrm{No}\leftrightarrow \left\{x{-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
83	81 82	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}$$
84		nulssgt	$$⊢\left\{x{-}_s{1}_s\right\}\in 𝒫\mathrm{No}\to \left\{x{-}_s{1}_s\right\}{\ll }_s\varnothing$$
85	83 84	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$$
86	39	a1i	$$⊢\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$$
87		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$$
88		df-1s	$$⊢1_s=\left\{0_s\right\}{|}_s\varnothing$$
89	88	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$$
90	85 86 87 89	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)$$
91	48	adantr	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x=\left\{x{-}_s{1}_s\right\}{|}_s\varnothing \right)\to x\in \mathrm{No}$$
92		pncans	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(x{+}_s{1}_s\right){-}_s{1}_s=x$$
93	91 22 92	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$$
94	93	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\}$$
95	94	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$$
96	78 90 95	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$$
97	96	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)$$
98	5 10 15 20 43 97	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$