Theorem n0scut 27943

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

Assertion

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

Proof of Theorem n0scut

Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝑦 = 0s → 𝑦 = 0s )
2		oveq1 7418	. . . . 5 ⊢ (𝑦 = 0s → (𝑦 -s 1s ) = ( 0s -s 1s ))
3	2	sneqd 4639	. . . 4 ⊢ (𝑦 = 0s → {(𝑦 -s 1s )} = {( 0s -s 1s )})
4	3	oveq1d 7426	. . 3 ⊢ (𝑦 = 0s → ({(𝑦 -s 1s )} |s ∅) = ({( 0s -s 1s )} |s ∅))
5	1, 4	eqeq12d 2746	. 2 ⊢ (𝑦 = 0s → (𝑦 = ({(𝑦 -s 1s )} |s ∅) ↔ 0s = ({( 0s -s 1s )} |s ∅)))
6		id 22	. . 3 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
7		oveq1 7418	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 -s 1s ) = (𝑥 -s 1s ))
8	7	sneqd 4639	. . . 4 ⊢ (𝑦 = 𝑥 → {(𝑦 -s 1s )} = {(𝑥 -s 1s )})
9	8	oveq1d 7426	. . 3 ⊢ (𝑦 = 𝑥 → ({(𝑦 -s 1s )} |s ∅) = ({(𝑥 -s 1s )} |s ∅))
10	6, 9	eqeq12d 2746	. 2 ⊢ (𝑦 = 𝑥 → (𝑦 = ({(𝑦 -s 1s )} |s ∅) ↔ 𝑥 = ({(𝑥 -s 1s )} |s ∅)))
11		id 22	. . 3 ⊢ (𝑦 = (𝑥 +s 1s ) → 𝑦 = (𝑥 +s 1s ))
12		oveq1 7418	. . . . 5 ⊢ (𝑦 = (𝑥 +s 1s ) → (𝑦 -s 1s ) = ((𝑥 +s 1s ) -s 1s ))
13	12	sneqd 4639	. . . 4 ⊢ (𝑦 = (𝑥 +s 1s ) → {(𝑦 -s 1s )} = {((𝑥 +s 1s ) -s 1s )})
14	13	oveq1d 7426	. . 3 ⊢ (𝑦 = (𝑥 +s 1s ) → ({(𝑦 -s 1s )} |s ∅) = ({((𝑥 +s 1s ) -s 1s )} |s ∅))
15	11, 14	eqeq12d 2746	. 2 ⊢ (𝑦 = (𝑥 +s 1s ) → (𝑦 = ({(𝑦 -s 1s )} |s ∅) ↔ (𝑥 +s 1s ) = ({((𝑥 +s 1s ) -s 1s )} |s ∅)))
16		id 22	. . 3 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
17		oveq1 7418	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 -s 1s ) = (𝐴 -s 1s ))
18	17	sneqd 4639	. . . 4 ⊢ (𝑦 = 𝐴 → {(𝑦 -s 1s )} = {(𝐴 -s 1s )})
19	18	oveq1d 7426	. . 3 ⊢ (𝑦 = 𝐴 → ({(𝑦 -s 1s )} |s ∅) = ({(𝐴 -s 1s )} |s ∅))
20	16, 19	eqeq12d 2746	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 = ({(𝑦 -s 1s )} |s ∅) ↔ 𝐴 = ({(𝐴 -s 1s )} |s ∅)))
21		0sno 27564	. . . . . . . 8 ⊢ 0s ∈ No
22		1sno 27565	. . . . . . . 8 ⊢ 1s ∈ No
23		subscl 27773	. . . . . . . 8 ⊢ (( 0s ∈ No ∧ 1s ∈ No ) → ( 0s -s 1s ) ∈ No )
24	21, 22, 23	mp2an 688	. . . . . . 7 ⊢ ( 0s -s 1s ) ∈ No
25	24	a1i 11	. . . . . 6 ⊢ (⊤ → ( 0s -s 1s ) ∈ No )
26	21	a1i 11	. . . . . 6 ⊢ (⊤ → 0s ∈ No )
27		0slt1s 27567	. . . . . . . 8 ⊢ 0s <s 1s
28		addslid 27690	. . . . . . . . 9 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
29	22, 28	ax-mp 5	. . . . . . . 8 ⊢ ( 0s +s 1s ) = 1s
30	27, 29	breqtrri 5174	. . . . . . 7 ⊢ 0s <s ( 0s +s 1s )
31	22	a1i 11	. . . . . . . 8 ⊢ (⊤ → 1s ∈ No )
32	26, 31, 26	sltsubaddd 27795	. . . . . . 7 ⊢ (⊤ → (( 0s -s 1s ) <s 0s ↔ 0s <s ( 0s +s 1s )))
33	30, 32	mpbiri 257	. . . . . 6 ⊢ (⊤ → ( 0s -s 1s ) <s 0s )
34	25, 26, 33	ssltsn 27530	. . . . 5 ⊢ (⊤ → {( 0s -s 1s )} <<s { 0s })
35	21	elexi 3492	. . . . . . . . 9 ⊢ 0s ∈ V
36	35	snelpw 5444	. . . . . . . 8 ⊢ ( 0s ∈ No ↔ { 0s } ∈ 𝒫 No )
37	21, 36	mpbi 229	. . . . . . 7 ⊢ { 0s } ∈ 𝒫 No
38		nulssgt 27536	. . . . . . 7 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
39	37, 38	ax-mp 5	. . . . . 6 ⊢ { 0s } <<s ∅
40	39	a1i 11	. . . . 5 ⊢ (⊤ → { 0s } <<s ∅)
41	34, 40	cuteq0 27570	. . . 4 ⊢ (⊤ → ({( 0s -s 1s )} |s ∅) = 0s )
42	41	mptru 1546	. . 3 ⊢ ({( 0s -s 1s )} |s ∅) = 0s
43	42	eqcomi 2739	. 2 ⊢ 0s = ({( 0s -s 1s )} |s ∅)
44		ovex 7444	. . . . . . . . . . 11 ⊢ (𝑥 -s 1s ) ∈ V
45		oveq1 7418	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 -s 1s ) → (𝑏 +s 1s ) = ((𝑥 -s 1s ) +s 1s ))
46	45	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 -s 1s ) → (𝑎 = (𝑏 +s 1s ) ↔ 𝑎 = ((𝑥 -s 1s ) +s 1s )))
47	44, 46	rexsn 4685	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s ) ↔ 𝑎 = ((𝑥 -s 1s ) +s 1s ))
48		n0ssno 27936	. . . . . . . . . . . . . 14 ⊢ ℕ0s ⊆ No
49	48	sseli 3977	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℕ0s → 𝑥 ∈ No )
50		npcans 27781	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ No ∧ 1s ∈ No ) → ((𝑥 -s 1s ) +s 1s ) = 𝑥)
51	49, 22, 50	sylancl 584	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℕ0s → ((𝑥 -s 1s ) +s 1s ) = 𝑥)
52	51	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ((𝑥 -s 1s ) +s 1s ) = 𝑥)
53	52	eqeq2d 2741	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (𝑎 = ((𝑥 -s 1s ) +s 1s ) ↔ 𝑎 = 𝑥))
54	47, 53	bitrid 282	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s ) ↔ 𝑎 = 𝑥))
55	54	alrimiv 1928	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ∀𝑎(∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s ) ↔ 𝑎 = 𝑥))
56		absn 4645	. . . . . . . 8 ⊢ ({𝑎 ∣ ∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s )} = {𝑥} ↔ ∀𝑎(∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s ) ↔ 𝑎 = 𝑥))
57	55, 56	sylibr 233	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → {𝑎 ∣ ∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s )} = {𝑥})
58		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑏 = 0s → (𝑥 +s 𝑏) = (𝑥 +s 0s ))
59	58	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑏 = 0s → (𝑎 = (𝑥 +s 𝑏) ↔ 𝑎 = (𝑥 +s 0s )))
60	35, 59	rexsn 4685	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏) ↔ 𝑎 = (𝑥 +s 0s ))
61	49	addsridd 27687	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℕ0s → (𝑥 +s 0s ) = 𝑥)
62	61	adantr 479	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (𝑥 +s 0s ) = 𝑥)
63	62	eqeq2d 2741	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (𝑎 = (𝑥 +s 0s ) ↔ 𝑎 = 𝑥))
64	60, 63	bitrid 282	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏) ↔ 𝑎 = 𝑥))
65	64	alrimiv 1928	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ∀𝑎(∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏) ↔ 𝑎 = 𝑥))
66		absn 4645	. . . . . . . 8 ⊢ ({𝑎 ∣ ∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏)} = {𝑥} ↔ ∀𝑎(∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏) ↔ 𝑎 = 𝑥))
67	65, 66	sylibr 233	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → {𝑎 ∣ ∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏)} = {𝑥})
68	57, 67	uneq12d 4163	. . . . . 6 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ({𝑎 ∣ ∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏)}) = ({𝑥} ∪ {𝑥}))
69		unidm 4151	. . . . . 6 ⊢ ({𝑥} ∪ {𝑥}) = {𝑥}
70	68, 69	eqtrdi 2786	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ({𝑎 ∣ ∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏)}) = {𝑥})
71		rex0 4356	. . . . . . . . 9 ⊢ ¬ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )
72	71	abf 4401	. . . . . . . 8 ⊢ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )} = ∅
73		rex0 4356	. . . . . . . . 9 ⊢ ¬ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)
74	73	abf 4401	. . . . . . . 8 ⊢ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)} = ∅
75	72, 74	uneq12i 4160	. . . . . . 7 ⊢ ({𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)}) = (∅ ∪ ∅)
76		un0 4389	. . . . . . 7 ⊢ (∅ ∪ ∅) = ∅
77	75, 76	eqtri 2758	. . . . . 6 ⊢ ({𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)}) = ∅
78	77	a1i 11	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ({𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)}) = ∅)
79	70, 78	oveq12d 7429	. . . 4 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (({𝑎 ∣ ∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏)}) |s ({𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)})) = ({𝑥} |s ∅))
80		subscl 27773	. . . . . . . . 9 ⊢ ((𝑥 ∈ No ∧ 1s ∈ No ) → (𝑥 -s 1s ) ∈ No )
81	49, 22, 80	sylancl 584	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ0s → (𝑥 -s 1s ) ∈ No )
82	81	adantr 479	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (𝑥 -s 1s ) ∈ No )
83	44	snelpw 5444	. . . . . . 7 ⊢ ((𝑥 -s 1s ) ∈ No ↔ {(𝑥 -s 1s )} ∈ 𝒫 No )
84	82, 83	sylib 217	. . . . . 6 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → {(𝑥 -s 1s )} ∈ 𝒫 No )
85		nulssgt 27536	. . . . . 6 ⊢ ({(𝑥 -s 1s )} ∈ 𝒫 No → {(𝑥 -s 1s )} <<s ∅)
86	84, 85	syl 17	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → {(𝑥 -s 1s )} <<s ∅)
87	39	a1i 11	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → { 0s } <<s ∅)
88		simpr 483	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → 𝑥 = ({(𝑥 -s 1s )} |s ∅))
89		df-1s 27563	. . . . . 6 ⊢ 1s = ({ 0s } |s ∅)
90	89	a1i 11	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → 1s = ({ 0s } |s ∅))
91	86, 87, 88, 90	addsunif 27724	. . . 4 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (𝑥 +s 1s ) = (({𝑎 ∣ ∃𝑏 ∈ {(𝑥 -s 1s )}𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ { 0s }𝑎 = (𝑥 +s 𝑏)}) |s ({𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑏 +s 1s )} ∪ {𝑎 ∣ ∃𝑏 ∈ ∅ 𝑎 = (𝑥 +s 𝑏)})))
92	49	adantr 479	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → 𝑥 ∈ No )
93		pncans 27779	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 1s ∈ No ) → ((𝑥 +s 1s ) -s 1s ) = 𝑥)
94	92, 22, 93	sylancl 584	. . . . . 6 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ((𝑥 +s 1s ) -s 1s ) = 𝑥)
95	94	sneqd 4639	. . . . 5 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → {((𝑥 +s 1s ) -s 1s )} = {𝑥})
96	95	oveq1d 7426	. . . 4 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → ({((𝑥 +s 1s ) -s 1s )} |s ∅) = ({𝑥} |s ∅))
97	79, 91, 96	3eqtr4d 2780	. . 3 ⊢ ((𝑥 ∈ ℕ0s ∧ 𝑥 = ({(𝑥 -s 1s )} |s ∅)) → (𝑥 +s 1s ) = ({((𝑥 +s 1s ) -s 1s )} |s ∅))
98	97	ex 411	. 2 ⊢ (𝑥 ∈ ℕ0s → (𝑥 = ({(𝑥 -s 1s )} |s ∅) → (𝑥 +s 1s ) = ({((𝑥 +s 1s ) -s 1s )} |s ∅)))
99	5, 10, 15, 20, 43, 98	n0sind 27942	1 ⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1537   = wceq 1539  ⊤wtru 1540   ∈ wcel 2104  {cab 2707  ∃wrex 3068   ∪ cun 3945  ∅c0 4321  𝒫 cpw 4601  {csn 4627   class class class wbr 5147  (class class class)co 7411   No csur 27379   <s cslt 27380   <<s csslt 27518   |s cscut 27520   0_s c0s 27560   1_s c1s 27561   +_s cadds 27681   -_s csubs 27734  ℕ_0scnn0s 27929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-nadd 8667  df-no 27382  df-slt 27383  df-bday 27384  df-sle 27484  df-sslt 27519  df-scut 27521  df-0s 27562  df-1s 27563  df-made 27579  df-old 27580  df-left 27582  df-right 27583  df-norec 27660  df-norec2 27671  df-adds 27682  df-negs 27735  df-subs 27736  df-n0s 27931

This theorem is referenced by:  n0ons  27944