Theorem sltssnb

Description: Surreal set less-than of two singletons. (Contributed by Scott Fenton, 18-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		sltssnb.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		sltssnb.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		snex	⊢ { 𝐴 } ∈ V
4		snex	⊢ { 𝐵 } ∈ V
5	3 4	pm3.2i	⊢ ( { 𝐴 } ∈ V ∧ { 𝐵 } ∈ V )
6		brslts	⊢ ( { 𝐴 } <<s { 𝐵 } ↔ ( ( { 𝐴 } ∈ V ∧ { 𝐵 } ∈ V ) ∧ ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) ) )
7	5 6	mpbiran	⊢ ( { 𝐴 } <<s { 𝐵 } ↔ ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) )
8		df-3an	⊢ ( ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) ↔ ( ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ) ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) )
9		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑦 ) )
10	9	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ { 𝐵 } 𝐴 <s 𝑦 ) )
11	10	ralsng	⊢ ( 𝐴 ∈ No → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ { 𝐵 } 𝐴 <s 𝑦 ) )
12	1 11	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ { 𝐵 } 𝐴 <s 𝑦 ) )
13	1	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ No )
14	2	snssd	⊢ ( 𝜑 → { 𝐵 } ⊆ No )
15	13 14	jca	⊢ ( 𝜑 → ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ) )
16	15	biantrurd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ ( ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ) ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) ) )
17		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 <s 𝑦 ↔ 𝐴 <s 𝐵 ) )
18	17	ralsng	⊢ ( 𝐵 ∈ No → ( ∀ 𝑦 ∈ { 𝐵 } 𝐴 <s 𝑦 ↔ 𝐴 <s 𝐵 ) )
19	2 18	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ { 𝐵 } 𝐴 <s 𝑦 ↔ 𝐴 <s 𝐵 ) )
20	12 16 19	3bitr3d	⊢ ( 𝜑 → ( ( ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ) ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) ↔ 𝐴 <s 𝐵 ) )
21	8 20	bitr2id	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( { 𝐴 } ⊆ No ∧ { 𝐵 } ⊆ No ∧ ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ) ) )
22	7 21	bitr4id	⊢ ( 𝜑 → ( { 𝐴 } <<s { 𝐵 } ↔ 𝐴 <s 𝐵 ) )