Theorem ssltsn

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

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

Proof

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