Theorem ssltsn

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

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

Proof

Step	Hyp	Ref	Expression
1		ssltsn.1	|- ( ph -> A e. No )
2		ssltsn.2	|- ( ph -> B e. No )
3		ssltsn.3	|- ( ph -> A
4		snex	|- { A } e. _V
5	4	a1i	|- ( ph -> { A } e. _V )
6		snex	|- { B } e. _V
7	6	a1i	|- ( ph -> { B } e. _V )
8	1	snssd	|- ( ph -> { A } C_ No )
9	2	snssd	|- ( ph -> { B } C_ No )
10		velsn	|- ( x e. { A } <-> x = A )
11		velsn	|- ( y e. { B } <-> y = B )
12		breq12	|- ( ( x = A /\ y = B ) -> ( x A
13	10 11 12	syl2anb	|- ( ( x e. { A } /\ y e. { B } ) -> ( x A
14	3 13	syl5ibrcom	|- ( ph -> ( ( x e. { A } /\ y e. { B } ) -> x
15	14	3impib	|- ( ( ph /\ x e. { A } /\ y e. { B } ) -> x
16	5 7 8 9 15	ssltd	|- ( ph -> { A } <