Theorem sltled

Description: Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025)

	Ref	Expression
Hypotheses	sltled.1	|- ( ph -> A e. No )
	sltled.2	|- ( ph -> B e. No )
	sltled.3	|- ( ph -> A
Assertion	sltled	|- ( ph -> A <_s B )

Proof

Step	Hyp	Ref	Expression
1		sltled.1	|- ( ph -> A e. No )
2		sltled.2	|- ( ph -> B e. No )
3		sltled.3	|- ( ph -> A
4	1 2	jca	|- ( ph -> ( A e. No /\ B e. No ) )
5		sltasym	|- ( ( A e. No /\ B e. No ) -> ( A -. B
6	4 3 5	sylc	|- ( ph -> -. B
7		slenlt	|- ( ( A e. No /\ B e. No ) -> ( A <_s B <-> -. B
8	1 2 7	syl2anc	|- ( ph -> ( A <_s B <-> -. B
9	6 8	mpbird	|- ( ph -> A <_s B )