Theorem n0s0m1

Description: Every non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	n0s0m1	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 = 0s ∨ ( 𝐴 -s 1s ) ∈ ℕ0s ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 0s → ( 𝑥 = 0s ↔ 0s = 0s ) )
2		oveq1	⊢ ( 𝑥 = 0s → ( 𝑥 -s 1s ) = ( 0s -s 1s ) )
3	2	eleq1d	⊢ ( 𝑥 = 0s → ( ( 𝑥 -s 1s ) ∈ ℕ0s ↔ ( 0s -s 1s ) ∈ ℕ0s ) )
4	1 3	orbi12d	⊢ ( 𝑥 = 0s → ( ( 𝑥 = 0s ∨ ( 𝑥 -s 1s ) ∈ ℕ0s ) ↔ ( 0s = 0s ∨ ( 0s -s 1s ) ∈ ℕ0s ) ) )
5		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 0s ↔ 𝑦 = 0s ) )
6		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 -s 1s ) = ( 𝑦 -s 1s ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 -s 1s ) ∈ ℕ0s ↔ ( 𝑦 -s 1s ) ∈ ℕ0s ) )
8	5 7	orbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 0s ∨ ( 𝑥 -s 1s ) ∈ ℕ0s ) ↔ ( 𝑦 = 0s ∨ ( 𝑦 -s 1s ) ∈ ℕ0s ) ) )
9		eqeq1	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑥 = 0s ↔ ( 𝑦 +s 1s ) = 0s ) )
10		oveq1	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑥 -s 1s ) = ( ( 𝑦 +s 1s ) -s 1s ) )
11	10	eleq1d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝑥 -s 1s ) ∈ ℕ0s ↔ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕ0s ) )
12	9 11	orbi12d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝑥 = 0s ∨ ( 𝑥 -s 1s ) ∈ ℕ0s ) ↔ ( ( 𝑦 +s 1s ) = 0s ∨ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕ0s ) ) )
13		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 0s ↔ 𝐴 = 0s ) )
14		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 -s 1s ) = ( 𝐴 -s 1s ) )
15	14	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 -s 1s ) ∈ ℕ0s ↔ ( 𝐴 -s 1s ) ∈ ℕ0s ) )
16	13 15	orbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 0s ∨ ( 𝑥 -s 1s ) ∈ ℕ0s ) ↔ ( 𝐴 = 0s ∨ ( 𝐴 -s 1s ) ∈ ℕ0s ) ) )
17		eqid	⊢ 0s = 0s
18	17	orci	⊢ ( 0s = 0s ∨ ( 0s -s 1s ) ∈ ℕ0s )
19		n0sno	⊢ ( 𝑦 ∈ ℕ0s → 𝑦 ∈ No )
20		1sno	⊢ 1s ∈ No
21		pncans	⊢ ( ( 𝑦 ∈ No ∧ 1s ∈ No ) → ( ( 𝑦 +s 1s ) -s 1s ) = 𝑦 )
22	19 20 21	sylancl	⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝑦 +s 1s ) -s 1s ) = 𝑦 )
23		id	⊢ ( 𝑦 ∈ ℕ0s → 𝑦 ∈ ℕ0s )
24	22 23	eqeltrd	⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕ0s )
25	24	olcd	⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝑦 +s 1s ) = 0s ∨ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕ0s ) )
26	25	a1d	⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝑦 = 0s ∨ ( 𝑦 -s 1s ) ∈ ℕ0s ) → ( ( 𝑦 +s 1s ) = 0s ∨ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕ0s ) ) )
27	4 8 12 16 18 26	n0sind	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 = 0s ∨ ( 𝐴 -s 1s ) ∈ ℕ0s ) )