Theorem n0scut

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

	Ref	Expression
Assertion	n0scut	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑦 = 0s → 𝑦 = 0s )
2		oveq1	⊢ ( 𝑦 = 0s → ( 𝑦 -s 1s ) = ( 0s -s 1s ) )
3	2	sneqd	⊢ ( 𝑦 = 0s → { ( 𝑦 -s 1s ) } = { ( 0s -s 1s ) } )
4	3	oveq1d	⊢ ( 𝑦 = 0s → ( { ( 𝑦 -s 1s ) } |s ∅ ) = ( { ( 0s -s 1s ) } |s ∅ ) )
5	1 4	eqeq12d	⊢ ( 𝑦 = 0s → ( 𝑦 = ( { ( 𝑦 -s 1s ) } |s ∅ ) ↔ 0s = ( { ( 0s -s 1s ) } |s ∅ ) ) )
6		id	⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
7		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 -s 1s ) = ( 𝑥 -s 1s ) )
8	7	sneqd	⊢ ( 𝑦 = 𝑥 → { ( 𝑦 -s 1s ) } = { ( 𝑥 -s 1s ) } )
9	8	oveq1d	⊢ ( 𝑦 = 𝑥 → ( { ( 𝑦 -s 1s ) } |s ∅ ) = ( { ( 𝑥 -s 1s ) } |s ∅ ) )
10	6 9	eqeq12d	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( { ( 𝑦 -s 1s ) } |s ∅ ) ↔ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) )
11		id	⊢ ( 𝑦 = ( 𝑥 +s 1s ) → 𝑦 = ( 𝑥 +s 1s ) )
12		oveq1	⊢ ( 𝑦 = ( 𝑥 +s 1s ) → ( 𝑦 -s 1s ) = ( ( 𝑥 +s 1s ) -s 1s ) )
13	12	sneqd	⊢ ( 𝑦 = ( 𝑥 +s 1s ) → { ( 𝑦 -s 1s ) } = { ( ( 𝑥 +s 1s ) -s 1s ) } )
14	13	oveq1d	⊢ ( 𝑦 = ( 𝑥 +s 1s ) → ( { ( 𝑦 -s 1s ) } |s ∅ ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
15	11 14	eqeq12d	⊢ ( 𝑦 = ( 𝑥 +s 1s ) → ( 𝑦 = ( { ( 𝑦 -s 1s ) } |s ∅ ) ↔ ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) ) )
16		id	⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
17		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 -s 1s ) = ( 𝐴 -s 1s ) )
18	17	sneqd	⊢ ( 𝑦 = 𝐴 → { ( 𝑦 -s 1s ) } = { ( 𝐴 -s 1s ) } )
19	18	oveq1d	⊢ ( 𝑦 = 𝐴 → ( { ( 𝑦 -s 1s ) } |s ∅ ) = ( { ( 𝐴 -s 1s ) } |s ∅ ) )
20	16 19	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = ( { ( 𝑦 -s 1s ) } |s ∅ ) ↔ 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) ) )
21		0sno	⊢ 0s ∈ No
22		1sno	⊢ 1s ∈ No
23		subscl	⊢ ( ( 0s ∈ No ∧ 1s ∈ No ) → ( 0s -s 1s ) ∈ No )
24	21 22 23	mp2an	⊢ ( 0s -s 1s ) ∈ No
25	24	a1i	⊢ ( ⊤ → ( 0s -s 1s ) ∈ No )
26	21	a1i	⊢ ( ⊤ → 0s ∈ No )
27		0slt1s	⊢ 0s <s 1s
28		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
29	22 28	ax-mp	⊢ ( 0s +s 1s ) = 1s
30	27 29	breqtrri	⊢ 0s <s ( 0s +s 1s )
31	22	a1i	⊢ ( ⊤ → 1s ∈ No )
32	26 31 26	sltsubaddd	⊢ ( ⊤ → ( ( 0s -s 1s ) <s 0s ↔ 0s <s ( 0s +s 1s ) ) )
33	30 32	mpbiri	⊢ ( ⊤ → ( 0s -s 1s ) <s 0s )
34	25 26 33	ssltsn	⊢ ( ⊤ → { ( 0s -s 1s ) } <<s { 0s } )
35	21	elexi	⊢ 0s ∈ V
36	35	snelpw	⊢ ( 0s ∈ No ↔ { 0s } ∈ 𝒫 No )
37	21 36	mpbi	⊢ { 0s } ∈ 𝒫 No
38		nulssgt	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
39	37 38	ax-mp	⊢ { 0s } <<s ∅
40	39	a1i	⊢ ( ⊤ → { 0s } <<s ∅ )
41	34 40	cuteq0	⊢ ( ⊤ → ( { ( 0s -s 1s ) } |s ∅ ) = 0s )
42	41	mptru	⊢ ( { ( 0s -s 1s ) } |s ∅ ) = 0s
43	42	eqcomi	⊢ 0s = ( { ( 0s -s 1s ) } |s ∅ )
44		ovex	⊢ ( 𝑥 -s 1s ) ∈ V
45		oveq1	⊢ ( 𝑏 = ( 𝑥 -s 1s ) → ( 𝑏 +s 1s ) = ( ( 𝑥 -s 1s ) +s 1s ) )
46	45	eqeq2d	⊢ ( 𝑏 = ( 𝑥 -s 1s ) → ( 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = ( ( 𝑥 -s 1s ) +s 1s ) ) )
47	44 46	rexsn	⊢ ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = ( ( 𝑥 -s 1s ) +s 1s ) )
48		n0sno	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
49		npcans	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑥 -s 1s ) +s 1s ) = 𝑥 )
50	48 22 49	sylancl	⊢ ( 𝑥 ∈ ℕ0s → ( ( 𝑥 -s 1s ) +s 1s ) = 𝑥 )
51	50	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ( 𝑥 -s 1s ) +s 1s ) = 𝑥 )
52	51	eqeq2d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑎 = ( ( 𝑥 -s 1s ) +s 1s ) ↔ 𝑎 = 𝑥 ) )
53	47 52	bitrid	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = 𝑥 ) )
54	53	alrimiv	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ∀ 𝑎 ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = 𝑥 ) )
55		absn	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } = { 𝑥 } ↔ ∀ 𝑎 ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = 𝑥 ) )
56	54 55	sylibr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } = { 𝑥 } )
57		oveq2	⊢ ( 𝑏 = 0s → ( 𝑥 +s 𝑏 ) = ( 𝑥 +s 0s ) )
58	57	eqeq2d	⊢ ( 𝑏 = 0s → ( 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = ( 𝑥 +s 0s ) ) )
59	35 58	rexsn	⊢ ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = ( 𝑥 +s 0s ) )
60	48	addsridd	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 +s 0s ) = 𝑥 )
61	60	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 +s 0s ) = 𝑥 )
62	61	eqeq2d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑎 = ( 𝑥 +s 0s ) ↔ 𝑎 = 𝑥 ) )
63	59 62	bitrid	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = 𝑥 ) )
64	63	alrimiv	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ∀ 𝑎 ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = 𝑥 ) )
65		absn	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } = { 𝑥 } ↔ ∀ 𝑎 ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = 𝑥 ) )
66	64 65	sylibr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } = { 𝑥 } )
67	56 66	uneq12d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ( { 𝑥 } ∪ { 𝑥 } ) )
68		unidm	⊢ ( { 𝑥 } ∪ { 𝑥 } ) = { 𝑥 }
69	67 68	eqtrdi	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) = { 𝑥 } )
70		rex0	⊢ ¬ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s )
71	70	abf	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } = ∅
72		rex0	⊢ ¬ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 )
73	72	abf	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } = ∅
74	71 73	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ( ∅ ∪ ∅ )
75		un0	⊢ ( ∅ ∪ ∅ ) = ∅
76	74 75	eqtri	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ∅
77	76	a1i	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ∅ )
78	69 77	oveq12d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) ) = ( { 𝑥 } |s ∅ ) )
79		subscl	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( 𝑥 -s 1s ) ∈ No )
80	48 22 79	sylancl	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 -s 1s ) ∈ No )
81	80	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 -s 1s ) ∈ No )
82	44	snelpw	⊢ ( ( 𝑥 -s 1s ) ∈ No ↔ { ( 𝑥 -s 1s ) } ∈ 𝒫 No )
83	81 82	sylib	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { ( 𝑥 -s 1s ) } ∈ 𝒫 No )
84		nulssgt	⊢ ( { ( 𝑥 -s 1s ) } ∈ 𝒫 No → { ( 𝑥 -s 1s ) } <<s ∅ )
85	83 84	syl	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { ( 𝑥 -s 1s ) } <<s ∅ )
86	39	a1i	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { 0s } <<s ∅ )
87		simpr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) )
88		df-1s	⊢ 1s = ( { 0s } |s ∅ )
89	88	a1i	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → 1s = ( { 0s } |s ∅ ) )
90	85 86 87 89	addsunif	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 +s 1s ) = ( ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) ) )
91	48	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → 𝑥 ∈ No )
92		pncans	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
93	91 22 92	sylancl	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
94	93	sneqd	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { ( ( 𝑥 +s 1s ) -s 1s ) } = { 𝑥 } )
95	94	oveq1d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) = ( { 𝑥 } |s ∅ ) )
96	78 90 95	3eqtr4d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
97	96	ex	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) ) )
98	5 10 15 20 43 97	n0sind	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) )