Theorem n0s0suc

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

	Ref	Expression
Assertion	n0s0suc	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝐴 = ( 𝑥 +s 1s ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑦 = 0s → ( 𝑦 = 0s ↔ 0s = 0s ) )
2		eqeq1	⊢ ( 𝑦 = 0s → ( 𝑦 = ( 𝑥 +s 1s ) ↔ 0s = ( 𝑥 +s 1s ) ) )
3	2	rexbidv	⊢ ( 𝑦 = 0s → ( ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 0s = ( 𝑥 +s 1s ) ) )
4	1 3	orbi12d	⊢ ( 𝑦 = 0s → ( ( 𝑦 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ) ↔ ( 0s = 0s ∨ ∃ 𝑥 ∈ ℕ0s 0s = ( 𝑥 +s 1s ) ) ) )
5		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 0s ↔ 𝑧 = 0s ) )
6		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( 𝑥 +s 1s ) ↔ 𝑧 = ( 𝑥 +s 1s ) ) )
7	6	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 𝑧 = ( 𝑥 +s 1s ) ) )
8	5 7	orbi12d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ) ↔ ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑧 = ( 𝑥 +s 1s ) ) ) )
9		eqeq1	⊢ ( 𝑦 = ( 𝑧 +s 1s ) → ( 𝑦 = 0s ↔ ( 𝑧 +s 1s ) = 0s ) )
10		eqeq1	⊢ ( 𝑦 = ( 𝑧 +s 1s ) → ( 𝑦 = ( 𝑥 +s 1s ) ↔ ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ) )
11	10	rexbidv	⊢ ( 𝑦 = ( 𝑧 +s 1s ) → ( ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ) )
12	9 11	orbi12d	⊢ ( 𝑦 = ( 𝑧 +s 1s ) → ( ( 𝑦 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ) ↔ ( ( 𝑧 +s 1s ) = 0s ∨ ∃ 𝑥 ∈ ℕ0s ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ) ) )
13		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 0s ↔ 𝐴 = 0s ) )
14		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = ( 𝑥 +s 1s ) ↔ 𝐴 = ( 𝑥 +s 1s ) ) )
15	14	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 𝐴 = ( 𝑥 +s 1s ) ) )
16	13 15	orbi12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑦 = ( 𝑥 +s 1s ) ) ↔ ( 𝐴 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝐴 = ( 𝑥 +s 1s ) ) ) )
17		eqid	⊢ 0s = 0s
18	17	orci	⊢ ( 0s = 0s ∨ ∃ 𝑥 ∈ ℕ0s 0s = ( 𝑥 +s 1s ) )
19		clel5	⊢ ( 𝑧 ∈ ℕ0s ↔ ∃ 𝑥 ∈ ℕ0s 𝑧 = 𝑥 )
20	19	biimpi	⊢ ( 𝑧 ∈ ℕ0s → ∃ 𝑥 ∈ ℕ0s 𝑧 = 𝑥 )
21		n0no	⊢ ( 𝑧 ∈ ℕ0s → 𝑧 ∈ No )
22		n0no	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
23		1no	⊢ 1s ∈ No
24		addscan2	⊢ ( ( 𝑧 ∈ No ∧ 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ↔ 𝑧 = 𝑥 ) )
25	23 24	mp3an3	⊢ ( ( 𝑧 ∈ No ∧ 𝑥 ∈ No ) → ( ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ↔ 𝑧 = 𝑥 ) )
26	21 22 25	syl2an	⊢ ( ( 𝑧 ∈ ℕ0s ∧ 𝑥 ∈ ℕ0s ) → ( ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ↔ 𝑧 = 𝑥 ) )
27	26	rexbidva	⊢ ( 𝑧 ∈ ℕ0s → ( ∃ 𝑥 ∈ ℕ0s ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 𝑧 = 𝑥 ) )
28	20 27	mpbird	⊢ ( 𝑧 ∈ ℕ0s → ∃ 𝑥 ∈ ℕ0s ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) )
29	28	olcd	⊢ ( 𝑧 ∈ ℕ0s → ( ( 𝑧 +s 1s ) = 0s ∨ ∃ 𝑥 ∈ ℕ0s ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ) )
30	29	a1d	⊢ ( 𝑧 ∈ ℕ0s → ( ( 𝑧 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑧 = ( 𝑥 +s 1s ) ) → ( ( 𝑧 +s 1s ) = 0s ∨ ∃ 𝑥 ∈ ℕ0s ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) ) ) )
31	4 8 12 16 18 30	n0sind	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝐴 = ( 𝑥 +s 1s ) ) )