Theorem sltssn

Description: Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Hypotheses	sltssn.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	sltssn.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	sltssn.3	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
Assertion	sltssn	⊢ ( 𝜑 → { 𝐴 } <<s { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		sltssn.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		sltssn.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		sltssn.3	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
4	1 2	sltssnb	⊢ ( 𝜑 → ( { 𝐴 } <<s { 𝐵 } ↔ 𝐴 <s 𝐵 ) )
5	3 4	mpbird	⊢ ( 𝜑 → { 𝐴 } <<s { 𝐵 } )