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	|- ( A e. NN0_s <-> ( A e. NN_s \/ A = 0s ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	|- ( -. A = 0s \/ A = 0s )
2		df-ne	|- ( A =/= 0s <-> -. A = 0s )
3	2	orbi1i	|- ( ( A =/= 0s \/ A = 0s ) <-> ( -. A = 0s \/ A = 0s ) )
4	1 3	mpbir	|- ( A =/= 0s \/ A = 0s )
5		ordir	|- ( ( ( A e. NN0_s /\ A =/= 0s ) \/ A = 0s ) <-> ( ( A e. NN0_s \/ A = 0s ) /\ ( A =/= 0s \/ A = 0s ) ) )
6	4 5	mpbiran2	|- ( ( ( A e. NN0_s /\ A =/= 0s ) \/ A = 0s ) <-> ( A e. NN0_s \/ A = 0s ) )
7		elnns	|- ( A e. NN_s <-> ( A e. NN0_s /\ A =/= 0s ) )
8	7	orbi1i	|- ( ( A e. NN_s \/ A = 0s ) <-> ( ( A e. NN0_s /\ A =/= 0s ) \/ A = 0s ) )
9		orc	|- ( A e. NN0_s -> ( A e. NN0_s \/ A = 0s ) )
10		id	|- ( A e. NN0_s -> A e. NN0_s )
11		id	|- ( A = 0s -> A = 0s )
12		0n0s	|- 0s e. NN0_s
13	11 12	eqeltrdi	|- ( A = 0s -> A e. NN0_s )
14	10 13	jaoi	|- ( ( A e. NN0_s \/ A = 0s ) -> A e. NN0_s )
15	9 14	impbii	|- ( A e. NN0_s <-> ( A e. NN0_s \/ A = 0s ) )
16	6 8 15	3bitr4ri	|- ( A e. NN0_s <-> ( A e. NN_s \/ A = 0s ) )