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		snex	⊢ { 𝐴 } ∈ V
5	4	a1i	⊢ ( 𝜑 → { 𝐴 } ∈ V )
6		snex	⊢ { 𝐵 } ∈ V
7	6	a1i	⊢ ( 𝜑 → { 𝐵 } ∈ V )
8	1	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ No )
9	2	snssd	⊢ ( 𝜑 → { 𝐵 } ⊆ No )
10		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
11		velsn	⊢ ( 𝑦 ∈ { 𝐵 } ↔ 𝑦 = 𝐵 )
12		breq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 <s 𝑦 ↔ 𝐴 <s 𝐵 ) )
13	10 11 12	syl2anb	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐵 } ) → ( 𝑥 <s 𝑦 ↔ 𝐴 <s 𝐵 ) )
14	3 13	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐵 } ) → 𝑥 <s 𝑦 ) )
15	14	3impib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐵 } ) → 𝑥 <s 𝑦 )
16	5 7 8 9 15	ssltd	⊢ ( 𝜑 → { 𝐴 } <<s { 𝐵 } )