Theorem rightpos

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

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

Proof

Step	Hyp	Ref	Expression
1		rightpos.1	$$⊢\phi \to A{\ll }_{s}B$$
2		rightpos.2	$$⊢\phi \to X=A{|}_{s}B$$
3		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
4		nulssgt	$$⊢\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	slerecd	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