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	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	rightpos.2	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
Assertion	rightpos	⊢ ( 𝜑 → ( 0s ≤s 𝑋 ↔ ∀ 𝑥𝑅 ∈ 𝐵 0s <s 𝑥𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rightpos.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		rightpos.2	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
3		0elpw	⊢ ∅ ∈ 𝒫 No
4		nulssgt	⊢ ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
5	3 4	mp1i	⊢ ( 𝜑 → ∅ <<s ∅ )
6		df-0s	⊢ 0s = ( ∅ |s ∅ )
7	6	a1i	⊢ ( 𝜑 → 0s = ( ∅ |s ∅ ) )
8	5 1 7 2	slerecd	⊢ ( 𝜑 → ( 0s ≤s 𝑋 ↔ ( ∀ 𝑥𝑅 ∈ 𝐵 0s <s 𝑥𝑅 ∧ ∀ 𝑥𝐿 ∈ ∅ 𝑥𝐿 <s 𝑋 ) ) )
9		ral0	⊢ ∀ 𝑥𝐿 ∈ ∅ 𝑥𝐿 <s 𝑋
10	9	biantru	⊢ ( ∀ 𝑥𝑅 ∈ 𝐵 0s <s 𝑥𝑅 ↔ ( ∀ 𝑥𝑅 ∈ 𝐵 0s <s 𝑥𝑅 ∧ ∀ 𝑥𝐿 ∈ ∅ 𝑥𝐿 <s 𝑋 ) )
11	8 10	bitr4di	⊢ ( 𝜑 → ( 0s ≤s 𝑋 ↔ ∀ 𝑥𝑅 ∈ 𝐵 0s <s 𝑥𝑅 ) )