Theorem rightge0

Description: A surreal is non-negative iff all its right options are positive. (Contributed by Scott Fenton, 1-Jan-2026)

	Ref	Expression
Hypotheses	rightge0.1	$$⊢\phi \to A{\ll }_{s}B$$
	rightge0.2	$$⊢\phi \to X=A{|}_{s}B$$
Assertion	rightge0	Could not format assertion : No typesetting found for |- ( ph -> ( 0s <_s X <-> A. xR e. B 0s

Proof

Step	Hyp	Ref	Expression
1		rightge0.1	$$⊢\phi \to A{\ll }_{s}B$$
2		rightge0.2	$$⊢\phi \to X=A{|}_{s}B$$
3		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
4		nulsgts	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
5	3 4	mp1i	$$⊢\phi \to \varnothing {\ll }_s\varnothing$$
6		df-0s	$$⊢0_s=\varnothing {|}_s\varnothing$$
7	6	a1i	$$⊢\phi \to 0_s=\varnothing {|}_s\varnothing$$
8	5 1 7 2	lesrecd	Could not format ( ph -> ( 0s <_s X <-> ( A. xR e. B 0s ( 0s <_s X <-> ( A. xR e. B 0s
9		ral0	Could not format A. xL e. (/) xL
10	9	biantru	Could not format ( A. xR e. B 0s ( A. xR e. B 0s ( A. xR e. B 0s
11	8 10	bitr4di	Could not format ( ph -> ( 0s <_s X <-> A. xR e. B 0s ( 0s <_s X <-> A. xR e. B 0s