Theorem eln0s

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

	Ref	Expression
Assertion	eln0s	⊢ ( 𝐴 ∈ ℕ0s ↔ ( 𝐴 ∈ ℕs ∨ 𝐴 = 0s ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	⊢ ( ¬ 𝐴 = 0s ∨ 𝐴 = 0s )
2		df-ne	⊢ ( 𝐴 ≠ 0s ↔ ¬ 𝐴 = 0s )
3	2	orbi1i	⊢ ( ( 𝐴 ≠ 0s ∨ 𝐴 = 0s ) ↔ ( ¬ 𝐴 = 0s ∨ 𝐴 = 0s ) )
4	1 3	mpbir	⊢ ( 𝐴 ≠ 0s ∨ 𝐴 = 0s )
5		ordir	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) ∨ 𝐴 = 0s ) ↔ ( ( 𝐴 ∈ ℕ0s ∨ 𝐴 = 0s ) ∧ ( 𝐴 ≠ 0s ∨ 𝐴 = 0s ) ) )
6	4 5	mpbiran2	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) ∨ 𝐴 = 0s ) ↔ ( 𝐴 ∈ ℕ0s ∨ 𝐴 = 0s ) )
7		elnns	⊢ ( 𝐴 ∈ ℕs ↔ ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) )
8	7	orbi1i	⊢ ( ( 𝐴 ∈ ℕs ∨ 𝐴 = 0s ) ↔ ( ( 𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ) ∨ 𝐴 = 0s ) )
9		orc	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s ∨ 𝐴 = 0s ) )
10		id	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ ℕ0s )
11		id	⊢ ( 𝐴 = 0s → 𝐴 = 0s )
12		0n0s	⊢ 0s ∈ ℕ0s
13	11 12	eqeltrdi	⊢ ( 𝐴 = 0s → 𝐴 ∈ ℕ0s )
14	10 13	jaoi	⊢ ( ( 𝐴 ∈ ℕ0s ∨ 𝐴 = 0s ) → 𝐴 ∈ ℕ0s )
15	9 14	impbii	⊢ ( 𝐴 ∈ ℕ0s ↔ ( 𝐴 ∈ ℕ0s ∨ 𝐴 = 0s ) )
16	6 8 15	3bitr4ri	⊢ ( 𝐴 ∈ ℕ0s ↔ ( 𝐴 ∈ ℕs ∨ 𝐴 = 0s ) )