Theorem n0cut

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

	Ref	Expression
Assertion	n0cut	⊢ ( 𝐴 ∈ ℕ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		0no	⊢ 0s ∈ No
22		1no	⊢ 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	26	ltsm1d	⊢ ( ⊤ → ( 0s -s 1s ) <s 0s )
28	25 27	cutneg	⊢ ( ⊤ → ( { ( 0s -s 1s ) } |s ∅ ) = 0s )
29	28	mptru	⊢ ( { ( 0s -s 1s ) } |s ∅ ) = 0s
30	29	eqcomi	⊢ 0s = ( { ( 0s -s 1s ) } |s ∅ )
31		ovex	⊢ ( 𝑥 -s 1s ) ∈ V
32		oveq1	⊢ ( 𝑏 = ( 𝑥 -s 1s ) → ( 𝑏 +s 1s ) = ( ( 𝑥 -s 1s ) +s 1s ) )
33	32	eqeq2d	⊢ ( 𝑏 = ( 𝑥 -s 1s ) → ( 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = ( ( 𝑥 -s 1s ) +s 1s ) ) )
34	31 33	rexsn	⊢ ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = ( ( 𝑥 -s 1s ) +s 1s ) )
35		n0no	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
36		npcans	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑥 -s 1s ) +s 1s ) = 𝑥 )
37	35 22 36	sylancl	⊢ ( 𝑥 ∈ ℕ0s → ( ( 𝑥 -s 1s ) +s 1s ) = 𝑥 )
38	37	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ( 𝑥 -s 1s ) +s 1s ) = 𝑥 )
39	38	eqeq2d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑎 = ( ( 𝑥 -s 1s ) +s 1s ) ↔ 𝑎 = 𝑥 ) )
40	34 39	bitrid	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = 𝑥 ) )
41	40	alrimiv	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ∀ 𝑎 ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = 𝑥 ) )
42		absn	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } = { 𝑥 } ↔ ∀ 𝑎 ( ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) ↔ 𝑎 = 𝑥 ) )
43	41 42	sylibr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } = { 𝑥 } )
44	21	elexi	⊢ 0s ∈ V
45		oveq2	⊢ ( 𝑏 = 0s → ( 𝑥 +s 𝑏 ) = ( 𝑥 +s 0s ) )
46	45	eqeq2d	⊢ ( 𝑏 = 0s → ( 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = ( 𝑥 +s 0s ) ) )
47	44 46	rexsn	⊢ ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = ( 𝑥 +s 0s ) )
48	35	addsridd	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 +s 0s ) = 𝑥 )
49	48	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 +s 0s ) = 𝑥 )
50	49	eqeq2d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑎 = ( 𝑥 +s 0s ) ↔ 𝑎 = 𝑥 ) )
51	47 50	bitrid	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = 𝑥 ) )
52	51	alrimiv	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ∀ 𝑎 ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = 𝑥 ) )
53		absn	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } = { 𝑥 } ↔ ∀ 𝑎 ( ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) ↔ 𝑎 = 𝑥 ) )
54	52 53	sylibr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } = { 𝑥 } )
55	43 54	uneq12d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ( { 𝑥 } ∪ { 𝑥 } ) )
56		unidm	⊢ ( { 𝑥 } ∪ { 𝑥 } ) = { 𝑥 }
57	55 56	eqtrdi	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) = { 𝑥 } )
58		rex0	⊢ ¬ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s )
59	58	abf	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } = ∅
60		rex0	⊢ ¬ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 )
61	60	abf	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } = ∅
62	59 61	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ( ∅ ∪ ∅ )
63		un0	⊢ ( ∅ ∪ ∅ ) = ∅
64	62 63	eqtri	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ∅
65	64	a1i	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) = ∅ )
66	57 65	oveq12d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) ) = ( { 𝑥 } |s ∅ ) )
67		subscl	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( 𝑥 -s 1s ) ∈ No )
68	35 22 67	sylancl	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 -s 1s ) ∈ No )
69	68	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 -s 1s ) ∈ No )
70	31	snelpw	⊢ ( ( 𝑥 -s 1s ) ∈ No ↔ { ( 𝑥 -s 1s ) } ∈ 𝒫 No )
71	69 70	sylib	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { ( 𝑥 -s 1s ) } ∈ 𝒫 No )
72		nulsgts	⊢ ( { ( 𝑥 -s 1s ) } ∈ 𝒫 No → { ( 𝑥 -s 1s ) } <<s ∅ )
73	71 72	syl	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { ( 𝑥 -s 1s ) } <<s ∅ )
74	44	snelpw	⊢ ( 0s ∈ No ↔ { 0s } ∈ 𝒫 No )
75	21 74	mpbi	⊢ { 0s } ∈ 𝒫 No
76		nulsgts	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
77	75 76	mp1i	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { 0s } <<s ∅ )
78		simpr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) )
79		df-1s	⊢ 1s = ( { 0s } |s ∅ )
80	79	a1i	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → 1s = ( { 0s } |s ∅ ) )
81	73 77 78 80	addsunif	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 +s 1s ) = ( ( { 𝑎 ∣ ∃ 𝑏 ∈ { ( 𝑥 -s 1s ) } 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ { 0s } 𝑎 = ( 𝑥 +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑏 +s 1s ) } ∪ { 𝑎 ∣ ∃ 𝑏 ∈ ∅ 𝑎 = ( 𝑥 +s 𝑏 ) } ) ) )
82	35	adantr	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → 𝑥 ∈ No )
83		pncans	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
84	82 22 83	sylancl	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
85	84	sneqd	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → { ( ( 𝑥 +s 1s ) -s 1s ) } = { 𝑥 } )
86	85	oveq1d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) = ( { 𝑥 } |s ∅ ) )
87	66 81 86	3eqtr4d	⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) ) → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
88	87	ex	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 = ( { ( 𝑥 -s 1s ) } |s ∅ ) → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) ) )
89	5 10 15 20 30 88	n0sind	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) )