Theorem ssltsnb

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

	Ref	Expression
Hypotheses	ssltsnb.1	|- ( ph -> A e. No )
	ssltsnb.2	|- ( ph -> B e. No )
Assertion	ssltsnb	|- ( ph -> ( { A } < A

Proof

Step	Hyp	Ref	Expression
1		ssltsnb.1	|- ( ph -> A e. No )
2		ssltsnb.2	|- ( ph -> B e. No )
3		snex	|- { A } e. _V
4		snex	|- { B } e. _V
5	3 4	pm3.2i	|- ( { A } e. _V /\ { B } e. _V )
6		brsslt	|- ( { A } < ( ( { A } e. _V /\ { B } e. _V ) /\ ( { A } C_ No /\ { B } C_ No /\ A. x e. { A } A. y e. { B } x
7	5 6	mpbiran	|- ( { A } < ( { A } C_ No /\ { B } C_ No /\ A. x e. { A } A. y e. { B } x
8		df-3an	|- ( ( { A } C_ No /\ { B } C_ No /\ A. x e. { A } A. y e. { B } x ( ( { A } C_ No /\ { B } C_ No ) /\ A. x e. { A } A. y e. { B } x
9		breq1	|- ( x = A -> ( x A
10	9	ralbidv	|- ( x = A -> ( A. y e. { B } x A. y e. { B } A
11	10	ralsng	|- ( A e. No -> ( A. x e. { A } A. y e. { B } x A. y e. { B } A
12	1 11	syl	|- ( ph -> ( A. x e. { A } A. y e. { B } x A. y e. { B } A
13	1	snssd	|- ( ph -> { A } C_ No )
14	2	snssd	|- ( ph -> { B } C_ No )
15	13 14	jca	|- ( ph -> ( { A } C_ No /\ { B } C_ No ) )
16	15	biantrurd	|- ( ph -> ( A. x e. { A } A. y e. { B } x ( ( { A } C_ No /\ { B } C_ No ) /\ A. x e. { A } A. y e. { B } x
17		breq2	|- ( y = B -> ( A A
18	17	ralsng	|- ( B e. No -> ( A. y e. { B } A A
19	2 18	syl	|- ( ph -> ( A. y e. { B } A A
20	12 16 19	3bitr3d	|- ( ph -> ( ( ( { A } C_ No /\ { B } C_ No ) /\ A. x e. { A } A. y e. { B } x A
21	8 20	bitr2id	|- ( ph -> ( A ( { A } C_ No /\ { B } C_ No /\ A. x e. { A } A. y e. { B } x
22	7 21	bitr4id	|- ( ph -> ( { A } < A