Theorem ssltd

Description: Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024)

	Ref	Expression
Hypotheses	ssltd.1	|- ( ph -> A e. V )
	ssltd.2	|- ( ph -> B e. W )
	ssltd.3	|- ( ph -> A C_ No )
	ssltd.4	|- ( ph -> B C_ No )
	ssltd.5	|- ( ( ph /\ x e. A /\ y e. B ) -> x
Assertion	ssltd	|- ( ph -> A <

Proof

Step	Hyp	Ref	Expression
1		ssltd.1	|- ( ph -> A e. V )
2		ssltd.2	|- ( ph -> B e. W )
3		ssltd.3	|- ( ph -> A C_ No )
4		ssltd.4	|- ( ph -> B C_ No )
5		ssltd.5	|- ( ( ph /\ x e. A /\ y e. B ) -> x
6	1	elexd	|- ( ph -> A e. _V )
7	2	elexd	|- ( ph -> B e. _V )
8	5	3expb	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> x
9	8	ralrimivva	|- ( ph -> A. x e. A A. y e. B x
10	3 4 9	3jca	|- ( ph -> ( A C_ No /\ B C_ No /\ A. x e. A A. y e. B x
11		brsslt	|- ( A < ( ( A e. _V /\ B e. _V ) /\ ( A C_ No /\ B C_ No /\ A. x e. A A. y e. B x
12	6 7 10 11	syl21anbrc	|- ( ph -> A <