Theorem sltlend

Description: Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Hypotheses	sltlen.1	|- ( ph -> A e. No )
	sltlen.2	|- ( ph -> B e. No )
Assertion	sltlend	|- ( ph -> ( A ( A <_s B /\ B =/= A ) ) )

Proof

Step	Hyp	Ref	Expression
1		sltlen.1	|- ( ph -> A e. No )
2		sltlen.2	|- ( ph -> B e. No )
3	1	adantr	|- ( ( ph /\ A A e. No )
4	2	adantr	|- ( ( ph /\ A B e. No )
5		simpr	|- ( ( ph /\ A A
6	3 4 5	sltled	|- ( ( ph /\ A A <_s B )
7	6	ex	|- ( ph -> ( A A <_s B ) )
8		sltne	|- ( ( A e. No /\ A B =/= A )
9	1 8	sylan	|- ( ( ph /\ A B =/= A )
10	9	ex	|- ( ph -> ( A B =/= A ) )
11	7 10	jcad	|- ( ph -> ( A ( A <_s B /\ B =/= A ) ) )
12		sleloe	|- ( ( A e. No /\ B e. No ) -> ( A <_s B <-> ( A
13	1 2 12	syl2anc	|- ( ph -> ( A <_s B <-> ( A
14		eqneqall	|- ( B = A -> ( B =/= A -> A
15	14	eqcoms	|- ( A = B -> ( B =/= A -> A
16	15	jao1i	|- ( ( A ( B =/= A -> A
17	13 16	syl6bi	|- ( ph -> ( A <_s B -> ( B =/= A -> A
18	17	impd	|- ( ph -> ( ( A <_s B /\ B =/= A ) -> A
19	11 18	impbid	|- ( ph -> ( A ( A <_s B /\ B =/= A ) ) )